Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. NEWS
  2. renamed notin_fset to not_fmember
  3. added author
  4. merged
  5. adapted Transfer_Debug from fmember to fempty
  6. renamed variables
  7. merged
  8. fixed lemma name
  9. redefined FSet.fmember as an abbreviation based on Set.member
  10. replaced some lemmas' implicit formulas by explicit ones to avoid silent changes
Changeset 78111:a6989a7d192a by desharna:
NEWS
The file was modified NEWS
Changeset 78110:776f6b85243f by desharna:
renamed notin_fset to not_fmember
The file was modified src/HOL/Library/FSet.thy
Changeset 78109:5c6db3d1b602 by desharna:
added author
The file was modified src/HOL/Library/FSet.thy
Changeset 78108:250785900816 by desharna:
merged
Changeset 78107:0366e49dab85 by desharna:
adapted Transfer_Debug from fmember to fempty
The file was modified src/HOL/ex/Transfer_Debug.thy
Changeset 78106:6fe9cdf547c4 by desharna:
renamed variables
The file was modified src/HOL/Library/FSet.thy
Changeset 78105:ab8310c0e6d9 by desharna:
merged
Changeset 78104:8122e865687e by desharna:
fixed lemma name
The file was modified src/HOL/Library/FSet.thy
Changeset 78103:0252d635bfb2 by desharna:
redefined FSet.fmember as an abbreviation based on Set.member
The file was modified src/HOL/Library/FSet.thy
The file was modified src/HOL/Probability/Fin_Map.thy
Changeset 78102:f40bc75b2a3f by desharna:
replaced some lemmas' implicit formulas by explicit ones to avoid silent changes
The file was modified src/HOL/Library/FSet.thy

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. merged
  2. adapted to Isabelle/0252d635bfb2
Changeset 13489:d34609a6a678 by desharna:
merged
Changeset 13488:0de1311fe42d by desharna:
adapted to Isabelle/0252d635bfb2
The file was modified thys/BNF_CC/DDS.thy
The file was modified thys/CakeML_Codegen/Backend/CakeML_Correctness.thy
The file was modified thys/CakeML_Codegen/Compiler/Compiler.thy
The file was modified thys/CakeML_Codegen/Compiler/Composition.thy
The file was modified thys/CakeML_Codegen/Rewriting/Rewriting_Pterm_Elim.thy
The file was modified thys/CakeML_Codegen/Rewriting/Rewriting_Sterm.thy
The file was modified thys/CakeML_Codegen/Terms/Pterm.thy
The file was modified thys/CakeML_Codegen/Terms/Sterm.thy
The file was modified thys/Coinductive_Languages/Context_Free_Grammar.thy
The file was modified thys/Core_DOM/common/classes/CharacterDataClass.thy
The file was modified thys/Core_DOM/common/classes/DocumentClass.thy
The file was modified thys/Core_DOM/common/classes/NodeClass.thy
The file was modified thys/Core_DOM/common/classes/ObjectClass.thy
The file was modified thys/Core_DOM/common/monads/BaseMonad.thy
The file was modified thys/Core_DOM/common/monads/CharacterDataMonad.thy
The file was modified thys/Core_DOM/common/monads/DocumentMonad.thy
The file was modified thys/Core_DOM/common/monads/ElementMonad.thy
The file was modified thys/Core_DOM/common/monads/NodeMonad.thy
The file was modified thys/Core_DOM/common/monads/ObjectMonad.thy
The file was modified thys/Core_DOM/standard/Core_DOM_Heap_WF.thy
The file was modified thys/Core_DOM/standard/classes/ElementClass.thy
The file was modified thys/Core_SC_DOM/common/classes/CharacterDataClass.thy
The file was modified thys/Core_SC_DOM/common/classes/DocumentClass.thy
The file was modified thys/Core_SC_DOM/common/classes/NodeClass.thy
The file was modified thys/Core_SC_DOM/common/classes/ObjectClass.thy
The file was modified thys/Core_SC_DOM/common/monads/BaseMonad.thy
The file was modified thys/Core_SC_DOM/common/monads/CharacterDataMonad.thy
The file was modified thys/Core_SC_DOM/common/monads/DocumentMonad.thy
The file was modified thys/Core_SC_DOM/common/monads/ElementMonad.thy
The file was modified thys/Core_SC_DOM/common/monads/NodeMonad.thy
The file was modified thys/Core_SC_DOM/common/monads/ObjectMonad.thy
The file was modified thys/Core_SC_DOM/safely_composable/Core_DOM_Heap_WF.thy
The file was modified thys/Core_SC_DOM/safely_composable/classes/ElementClass.thy
The file was modified thys/DOM_Components/Core_DOM_Components.thy
The file was modified thys/Decl_Sem_Fun_PL/DenotCompleteFSet.thy
The file was modified thys/Decl_Sem_Fun_PL/DenotSoundFSet.thy
The file was modified thys/Decl_Sem_Fun_PL/ValuesFSetProps.thy
The file was modified thys/Extended_Finite_State_Machine_Inference/Inference.thy
The file was modified thys/Extended_Finite_State_Machines/EFSM.thy
The file was modified thys/Extended_Finite_State_Machines/EFSM_LTL.thy
The file was modified thys/Extended_Finite_State_Machines/FSet_Utils.thy
The file was modified thys/Extended_Finite_State_Machines/examples/Drinks_Machine.thy
The file was modified thys/FO_Theory_Rewriting/Closure/GTT_RRn.thy
The file was modified thys/FO_Theory_Rewriting/Closure/TA_Clousure_Const.thy
The file was modified thys/FO_Theory_Rewriting/FOR_Check.thy
The file was modified thys/FO_Theory_Rewriting/FOR_Check_Impl.thy
The file was modified thys/FO_Theory_Rewriting/Primitives/LV_to_GTT.thy
The file was modified thys/FO_Theory_Rewriting/Primitives/NF.thy
The file was modified thys/FO_Theory_Rewriting/Primitives/NF_Impl.thy
The file was modified thys/FO_Theory_Rewriting/Util/Tree_Automata_Derivation_Split.thy
The file was modified thys/FSM_Tests/EquivalenceTesting/Simple_Convergence_Graph.thy
The file was modified thys/FSM_Tests/FSM.thy
The file was modified thys/FSM_Tests/Minimisation.thy
The file was modified thys/FSM_Tests/Observability.thy
The file was modified thys/Factored_Transition_System_Bounding/FactoredSystem.thy
The file was modified thys/Factored_Transition_System_Bounding/SystemAbstraction.thy
The file was modified thys/Formula_Derivatives/WS1S_Alt_Formula.thy
The file was modified thys/Formula_Derivatives/WS1S_Formula.thy
The file was modified thys/Formula_Derivatives/WS1S_Prelim.thy
The file was modified thys/Incredible_Proof_Machine/Abstract_Rules_To_Incredible.thy
The file was modified thys/Incredible_Proof_Machine/Build_Incredible_Tree.thy
The file was modified thys/Incredible_Proof_Machine/Incredible_Completeness.thy
The file was modified thys/Incredible_Proof_Machine/Incredible_Correctness.thy
The file was modified thys/Incredible_Proof_Machine/Incredible_Deduction.thy
The file was modified thys/Incredible_Proof_Machine/Incredible_Signatures.thy
The file was modified thys/Incredible_Proof_Machine/Incredible_Trees.thy
The file was modified thys/Incredible_Proof_Machine/Indexed_FSet.thy
The file was modified thys/IsaNet/infrastructure/Abstract_XOR.thy
The file was modified thys/IsaNet/infrastructure/Message.thy
The file was modified thys/IsaNet/instances/Anapaya_SCION.thy
The file was modified thys/LTL/Disjunctive_Normal_Form.thy
The file was modified thys/LTL_Normal_Form/Normal_Form_Code_Export.thy
The file was modified thys/Linear_Programming/Matrix_LinPoly.thy
The file was modified thys/MiniSail/SyntaxL.thy
The file was modified thys/Nested_Multisets_Ordinals/Unary_PCF.thy
The file was modified thys/Nominal2/Nominal2_Base.thy
The file was modified thys/PAC_Checker/Finite_Map_Multiset.thy
The file was modified thys/PAC_Checker/PAC_Map_Rel.thy
The file was modified thys/Query_Optimization/Dtree.thy
The file was modified thys/Query_Optimization/IKKBZ.thy
The file was modified thys/Query_Optimization/IKKBZ_Optimality.thy
The file was modified thys/Query_Optimization/List_Dtree.thy
The file was modified thys/Regular_Tree_Relations/GTT_Compose.thy
The file was modified thys/Regular_Tree_Relations/GTT_Transitive_Closure.thy
The file was modified thys/Regular_Tree_Relations/Horn_Setup/Horn_Fset.thy
The file was modified thys/Regular_Tree_Relations/Pair_Automaton.thy
The file was modified thys/Regular_Tree_Relations/RR2_Infinite.thy
The file was modified thys/Regular_Tree_Relations/RR2_Infinite_Q_infinity.thy
The file was modified thys/Regular_Tree_Relations/RRn_Automata.thy
The file was modified thys/Regular_Tree_Relations/Regular_Relation_Abstract_Impl.thy
The file was modified thys/Regular_Tree_Relations/Regular_Relation_Impl.thy
The file was modified thys/Regular_Tree_Relations/Tree_Automata/Myhill_Nerode.thy
The file was modified thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata.thy
The file was modified thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Abstract_Impl.thy
The file was modified thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Complement.thy
The file was modified thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Det.thy
The file was modified thys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Impl.thy
The file was modified thys/Ribbon_Proofs/Ribbons_Graphical_Soundness.thy
The file was modified thys/Ribbon_Proofs/Ribbons_Interfaces.thy
The file was modified thys/SC_DOM_Components/Core_DOM_DOM_Components.thy
The file was modified thys/SC_DOM_Components/Core_DOM_SC_DOM_Components.thy
The file was modified thys/SC_DOM_Components/Shadow_DOM_SC_DOM_Components.thy
The file was modified thys/Safe_OCL/Finite_Map_Ext.thy
The file was modified thys/Safe_OCL/OCL_Typing.thy
The file was modified thys/Safe_OCL/Object_Model.thy
The file was modified thys/Shadow_DOM/Shadow_DOM.thy
The file was modified thys/Shadow_DOM/classes/ShadowRootClass.thy
The file was modified thys/Shadow_DOM/monads/ShadowRootMonad.thy
The file was modified thys/Shadow_SC_DOM/Shadow_DOM.thy
The file was modified thys/Shadow_SC_DOM/classes/ShadowRootClass.thy
The file was modified thys/Shadow_SC_DOM/monads/ShadowRootMonad.thy
The file was modified thys/Simplex/Linear_Poly_Maps.thy
The file was modified thys/Solidity/Statements.thy
The file was modified thys/UTP/toolkit/FSet_Extra.thy