Diffusion afp-devel ab05f9116530

replaced fmember.rep_eq by fmember_iff_member_fset
ab05f9116530
Actions

Description

replaced fmember.rep_eq by fmember_iff_member_fset

Details

Provenance

desharna

Authored on

Parents

rAFP1fea1f554ccf: adapted to Isabelle/457f1cba78fb

Branches

Unknown

Tags

Unknown

Event Timeline

desharna committed rAFPab05f9116530: replaced fmember.rep_eq by fmember_iff_member_fset.Oct 18 2022, 7:58 AM

Changes (71)

Path

Size

thys/

CakeML_Codegen/

Compiler/

Compiler.thy

Composition.thy

Rewriting/

Rewriting_Pterm_Elim.thy

Rewriting_Sterm.thy

Terms/

Pterm.thy

Sterm.thy

Coinductive_Languages/

Context_Free_Grammar.thy

Core_DOM/

common/

classes/

CharacterDataClass.thy

monads/

standard/

Core_SC_DOM/

common/

classes/

CharacterDataClass.thy

monads/

safely_composable/

Decl_Sem_Fun_PL/

Extended_Finite_State_Machines/

EFSM.thy

FSet_Utils.thy

FO_Theory_Rewriting/

Closure/

TA_Clousure_Const.thy

Primitives/

FSM_Tests/

EquivalenceTesting/

Simple_Convergence_Graph.thy

FSM.thy

Minimisation.thy

Observability.thy

Factored_Transition_System_Bounding/

FactoredSystem.thy

Formula_Derivatives/

WS1S_Alt_Formula.thy

WS1S_Formula.thy

Incredible_Proof_Machine/

Abstract_Rules_To_Incredible.thy

Build_Incredible_Tree.thy

Incredible_Completeness.thy

Incredible_Correctness.thy

Incredible_Signatures.thy

Incredible_Trees.thy

Indexed_FSet.thy

IsaNet/

infrastructure/

Abstract_XOR.thy

Message.thy

Nested_Multisets_Ordinals/

Unary_PCF.thy

PAC_Checker/

Finite_Map_Multiset.thy

PAC_Map_Rel.thy

Regular_Tree_Relations/

GTT_Compose.thy

GTT_Transitive_Closure.thy

Horn_Setup/

Horn_Fset.thy

Pair_Automaton.thy

RR2_Infinite_Q_infinity.thy

RRn_Automata.thy

Regular_Relation_Abstract_Impl.thy

Regular_Relation_Impl.thy

Tree_Automata/

Tree_Automata.thy

Tree_Automata_Abstract_Impl.thy

Tree_Automata_Complement.thy

Tree_Automata_Det.thy

Tree_Automata_Impl.thy

Ribbon_Proofs/

Ribbons_Graphical_Soundness.thy

Ribbons_Interfaces.thy

SC_DOM_Components/

Core_DOM_DOM_Components.thy

Core_DOM_SC_DOM_Components.thy

Shadow_DOM_SC_DOM_Components.thy

Safe_OCL/

Shadow_DOM/

monads/

Shadow_SC_DOM/

UTP/

toolkit/

FSet_Extra.thy

rAFPab05f9116530

View Options

thys/CakeML_Codegen/Compiler/Compiler.thy

View Options

thys/CakeML_Codegen/Compiler/Composition.thy

View Options

thys/CakeML_Codegen/Rewriting/Rewriting_Pterm_Elim.thy

View Options

thys/CakeML_Codegen/Rewriting/Rewriting_Sterm.thy

View Options

thys/CakeML_Codegen/Terms/Pterm.thy

View Options

thys/CakeML_Codegen/Terms/Sterm.thy

View Options

thys/Coinductive_Languages/Context_Free_Grammar.thy

View Options

thys/Core_DOM/common/classes/CharacterDataClass.thy

View Options

thys/Core_DOM/common/classes/DocumentClass.thy

View Options

thys/Core_DOM/common/classes/NodeClass.thy

View Options

thys/Core_DOM/common/monads/DocumentMonad.thy

View Options

thys/Core_DOM/common/monads/ObjectMonad.thy

View Options

thys/Core_DOM/standard/Core_DOM_Heap_WF.thy

View Options

thys/Core_SC_DOM/common/classes/CharacterDataClass.thy

View Options

thys/Core_SC_DOM/common/classes/DocumentClass.thy

View Options

thys/Core_SC_DOM/common/classes/NodeClass.thy

View Options

thys/Core_SC_DOM/common/monads/DocumentMonad.thy

View Options

thys/Core_SC_DOM/common/monads/ObjectMonad.thy

View Options

thys/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy

View Options

thys/Decl_Sem_Fun_PL/ValuesFSetProps.thy

View Options

thys/Extended_Finite_State_Machines/EFSM.thy

View Options

thys/Extended_Finite_State_Machines/FSet_Utils.thy

View Options

thys/FO_Theory_Rewriting/Closure/TA_Clousure_Const.thy

View Options

thys/FO_Theory_Rewriting/FOR_Check.thy

View Options

thys/FO_Theory_Rewriting/FOR_Check_Impl.thy

View Options

thys/FO_Theory_Rewriting/Primitives/LV_to_GTT.thy

View Options

thys/FO_Theory_Rewriting/Primitives/NF.thy

View Options

thys/FO_Theory_Rewriting/Primitives/NF_Impl.thy

View Options

thys/FSM_Tests/EquivalenceTesting/Simple_Convergence_Graph.thy

View Options

thys/FSM_Tests/FSM.thy

View Options

thys/FSM_Tests/Minimisation.thy

View Options

thys/FSM_Tests/Observability.thy

View Options

thys/Factored_Transition_System_Bounding/FactoredSystem.thy

View Options

thys/Formula_Derivatives/WS1S_Alt_Formula.thy

View Options

thys/Formula_Derivatives/WS1S_Formula.thy

View Options

thys/Incredible_Proof_Machine/Abstract_Rules_To_Incredible.thy

View Options

thys/Incredible_Proof_Machine/Build_Incredible_Tree.thy

View Options

thys/Incredible_Proof_Machine/Incredible_Completeness.thy

View Options

thys/Incredible_Proof_Machine/Incredible_Correctness.thy

View Options

thys/Incredible_Proof_Machine/Incredible_Signatures.thy

View Options

thys/Incredible_Proof_Machine/Incredible_Trees.thy

View Options

thys/Incredible_Proof_Machine/Indexed_FSet.thy

View Options

thys/IsaNet/infrastructure/Abstract_XOR.thy

View Options

thys/IsaNet/infrastructure/Message.thy

View Options

thys/Nested_Multisets_Ordinals/Unary_PCF.thy

View Options

thys/PAC_Checker/Finite_Map_Multiset.thy

View Options

thys/PAC_Checker/PAC_Map_Rel.thy

View Options

thys/Regular_Tree_Relations/GTT_Compose.thy

View Options

thys/Regular_Tree_Relations/GTT_Transitive_Closure.thy

View Options

thys/Regular_Tree_Relations/Horn_Setup/Horn_Fset.thy

View Options

thys/Regular_Tree_Relations/Pair_Automaton.thy

View Options

thys/Regular_Tree_Relations/RR2_Infinite_Q_infinity.thy

View Options

thys/Regular_Tree_Relations/RRn_Automata.thy

View Options

thys/Regular_Tree_Relations/Regular_Relation_Abstract_Impl.thy

View Options

thys/Regular_Tree_Relations/Regular_Relation_Impl.thy

View Options

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata.thy

View Options

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Abstract_Impl.thy

View Options

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Complement.thy

View Options

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Det.thy

View Options

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Impl.thy

View Options

thys/Ribbon_Proofs/Ribbons_Graphical_Soundness.thy

View Options

thys/Ribbon_Proofs/Ribbons_Interfaces.thy

View Options

thys/SC_DOM_Components/Core_DOM_DOM_Components.thy

View Options

thys/SC_DOM_Components/Core_DOM_SC_DOM_Components.thy

View Options

thys/SC_DOM_Components/Shadow_DOM_SC_DOM_Components.thy

View Options

thys/Safe_OCL/Finite_Map_Ext.thy

View Options

thys/Safe_OCL/Object_Model.thy

View Options

thys/Shadow_DOM/Shadow_DOM.thy

View Options

thys/Shadow_DOM/monads/ShadowRootMonad.thy

View Options

thys/Shadow_SC_DOM/Shadow_DOM.thy

View Options

thys/UTP/toolkit/FSet_Extra.thy

replaced fmember.rep_eq by fmember_iff_member_fsetab05f9116530Actions

Description

Details

Event Timeline

Changes (71)

rAFPab05f9116530

thys/CakeML_Codegen/Compiler/Compiler.thy

thys/CakeML_Codegen/Compiler/Composition.thy

thys/CakeML_Codegen/Rewriting/Rewriting_Pterm_Elim.thy

thys/CakeML_Codegen/Rewriting/Rewriting_Sterm.thy

thys/CakeML_Codegen/Terms/Pterm.thy

thys/CakeML_Codegen/Terms/Sterm.thy

thys/Coinductive_Languages/Context_Free_Grammar.thy

thys/Core_DOM/common/classes/CharacterDataClass.thy

thys/Core_DOM/common/classes/DocumentClass.thy

thys/Core_DOM/common/classes/NodeClass.thy

thys/Core_DOM/common/monads/DocumentMonad.thy

thys/Core_DOM/common/monads/ObjectMonad.thy

thys/Core_DOM/standard/Core_DOM_Heap_WF.thy

thys/Core_SC_DOM/common/classes/CharacterDataClass.thy

thys/Core_SC_DOM/common/classes/DocumentClass.thy

thys/Core_SC_DOM/common/classes/NodeClass.thy

thys/Core_SC_DOM/common/monads/DocumentMonad.thy

thys/Core_SC_DOM/common/monads/ObjectMonad.thy

thys/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy

thys/Decl_Sem_Fun_PL/ValuesFSetProps.thy

thys/Extended_Finite_State_Machines/EFSM.thy

thys/Extended_Finite_State_Machines/FSet_Utils.thy

thys/FO_Theory_Rewriting/Closure/TA_Clousure_Const.thy

thys/FO_Theory_Rewriting/FOR_Check.thy

thys/FO_Theory_Rewriting/FOR_Check_Impl.thy

thys/FO_Theory_Rewriting/Primitives/LV_to_GTT.thy

thys/FO_Theory_Rewriting/Primitives/NF.thy

thys/FO_Theory_Rewriting/Primitives/NF_Impl.thy

thys/FSM_Tests/EquivalenceTesting/Simple_Convergence_Graph.thy

thys/FSM_Tests/FSM.thy

thys/FSM_Tests/Minimisation.thy

thys/FSM_Tests/Observability.thy

thys/Factored_Transition_System_Bounding/FactoredSystem.thy

thys/Formula_Derivatives/WS1S_Alt_Formula.thy

thys/Formula_Derivatives/WS1S_Formula.thy

thys/Incredible_Proof_Machine/Abstract_Rules_To_Incredible.thy

thys/Incredible_Proof_Machine/Build_Incredible_Tree.thy

thys/Incredible_Proof_Machine/Incredible_Completeness.thy

thys/Incredible_Proof_Machine/Incredible_Correctness.thy

thys/Incredible_Proof_Machine/Incredible_Signatures.thy

thys/Incredible_Proof_Machine/Incredible_Trees.thy

thys/Incredible_Proof_Machine/Indexed_FSet.thy

thys/IsaNet/infrastructure/Abstract_XOR.thy

thys/IsaNet/infrastructure/Message.thy

thys/Nested_Multisets_Ordinals/Unary_PCF.thy

thys/PAC_Checker/Finite_Map_Multiset.thy

thys/PAC_Checker/PAC_Map_Rel.thy

thys/Regular_Tree_Relations/GTT_Compose.thy

thys/Regular_Tree_Relations/GTT_Transitive_Closure.thy

thys/Regular_Tree_Relations/Horn_Setup/Horn_Fset.thy

thys/Regular_Tree_Relations/Pair_Automaton.thy

thys/Regular_Tree_Relations/RR2_Infinite_Q_infinity.thy

thys/Regular_Tree_Relations/RRn_Automata.thy

thys/Regular_Tree_Relations/Regular_Relation_Abstract_Impl.thy

thys/Regular_Tree_Relations/Regular_Relation_Impl.thy

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata.thy

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Abstract_Impl.thy

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Complement.thy

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Det.thy

thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Impl.thy

thys/Ribbon_Proofs/Ribbons_Graphical_Soundness.thy

thys/Ribbon_Proofs/Ribbons_Interfaces.thy

thys/SC_DOM_Components/Core_DOM_DOM_Components.thy

thys/SC_DOM_Components/Core_DOM_SC_DOM_Components.thy

thys/SC_DOM_Components/Shadow_DOM_SC_DOM_Components.thy

thys/Safe_OCL/Finite_Map_Ext.thy

thys/Safe_OCL/Object_Model.thy

thys/Shadow_DOM/Shadow_DOM.thy

thys/Shadow_DOM/monads/ShadowRootMonad.thy

thys/Shadow_SC_DOM/Shadow_DOM.thy

thys/UTP/toolkit/FSet_Extra.thy

replaced fmember.rep_eq by fmember_iff_member_fset
ab05f9116530
Actions