Changes

Summary

merged
more canonical names

Changeset 6370:5fa209e31f09 by nipkow: merged
Changeset 6369:355af4cabf7f by nipkow: more canonical names
The file was modified	`thys/AODV/Aodv_Data.thy` (diff)
The file was modified	`thys/AODV/Fresher.thy` (diff)
The file was modified	`thys/AODV/Global_Invariants.thy` (diff)
The file was modified	`thys/AODV/Seq_Invariants.thy` (diff)
The file was modified	`thys/AODV/variants/a_norreqid/A_Aodv_Data.thy` (diff)
The file was modified	`thys/AODV/variants/a_norreqid/A_Fresher.thy` (diff)
The file was modified	`thys/AODV/variants/a_norreqid/A_Global_Invariants.thy` (diff)
The file was modified	`thys/AODV/variants/a_norreqid/A_Seq_Invariants.thy` (diff)
The file was modified	`thys/AODV/variants/b_fwdrreps/B_Aodv_Data.thy` (diff)
The file was modified	`thys/AODV/variants/b_fwdrreps/B_Fresher.thy` (diff)
The file was modified	`thys/AODV/variants/b_fwdrreps/B_Global_Invariants.thy` (diff)
The file was modified	`thys/AODV/variants/b_fwdrreps/B_Seq_Invariants.thy` (diff)
The file was modified	`thys/AODV/variants/c_gtobcast/C_Aodv_Data.thy` (diff)
The file was modified	`thys/AODV/variants/c_gtobcast/C_Fresher.thy` (diff)
The file was modified	`thys/AODV/variants/c_gtobcast/C_Global_Invariants.thy` (diff)
The file was modified	`thys/AODV/variants/c_gtobcast/C_Seq_Invariants.thy` (diff)
The file was modified	`thys/AODV/variants/d_fwdrreqs/D_Aodv_Data.thy` (diff)
The file was modified	`thys/AODV/variants/d_fwdrreqs/D_Fresher.thy` (diff)
The file was modified	`thys/AODV/variants/d_fwdrreqs/D_Global_Invariants.thy` (diff)
The file was modified	`thys/AODV/variants/d_fwdrreqs/D_Seq_Invariants.thy` (diff)
The file was modified	`thys/AODV/variants/e_all_abcd/E_Aodv_Data.thy` (diff)
The file was modified	`thys/AODV/variants/e_all_abcd/E_Fresher.thy` (diff)
The file was modified	`thys/AODV/variants/e_all_abcd/E_Global_Invariants.thy` (diff)
The file was modified	`thys/AODV/variants/e_all_abcd/E_Seq_Invariants.thy` (diff)
The file was modified	`thys/AVL-Trees/AVL2.thy` (diff)
The file was modified	`thys/AWN/Inv_Cterms.thy` (diff)
The file was modified	`thys/Abortable_Linearizable_Modules/Consensus.thy` (diff)
The file was modified	`thys/Abortable_Linearizable_Modules/IOA.thy` (diff)
The file was modified	`thys/Abortable_Linearizable_Modules/Idempotence.thy` (diff)
The file was modified	`thys/Abortable_Linearizable_Modules/RDR.thy` (diff)
The file was modified	`thys/Abortable_Linearizable_Modules/SLin.thy` (diff)
The file was modified	`thys/Abortable_Linearizable_Modules/Simulations.thy` (diff)
The file was modified	`thys/Abstract-Hoare-Logics/Proc/PHoareTotal.thy` (diff)
The file was modified	`thys/Abstract-Hoare-Logics/Proc/PLang.thy` (diff)
The file was modified	`thys/Abstract-Hoare-Logics/Procs/PsHoareTotal.thy` (diff)
The file was modified	`thys/Abstract-Hoare-Logics/Procs/PsLang.thy` (diff)
The file was modified	`thys/Abstract-Hoare-Logics/While/Hoare.thy` (diff)
The file was modified	`thys/Abstract-Hoare-Logics/While/HoareTotal.thy` (diff)
The file was modified	`thys/Abstract-Hoare-Logics/While/Lang.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Affine_Approximation.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Affine_Code.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Affine_Form.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Counterclockwise.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Counterclockwise_2D_Strict.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Intersection.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Polygon.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Approximation.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Asymptotics.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Library.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Method.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Real.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Master_Theorem.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Master_Theorem_Examples.thy` (diff)
The file was modified	`thys/Akra_Bazzi/akra_bazzi.ML` (diff)
The file was modified	`thys/Akra_Bazzi/akra_bazzi_approximation.ML` (diff)
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Factorization.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Roots.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Show_Real_Alg.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Sturm_Rat.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Lemmas_log.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Pairing_Heap_List.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Environment.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Environment_Algebra.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Examples.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Functor.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_List.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Option.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_PMF.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Set.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Star.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_State.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Stream.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Sum.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Beta_Eta.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Joinable.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Tree_Relabelling.thy` (diff)
The file was modified	`thys/ArrowImpossibilityGS/Thys/Arrow_Utility.thy` (diff)
The file was modified	`thys/ArrowImpossibilityGS/Thys/GS.thy` (diff)
The file was modified	`thys/AutoFocus-Stream/AF_Stream.thy` (diff)
The file was modified	`thys/AutoFocus-Stream/AF_Stream_Exec.thy` (diff)
The file was modified	`thys/AutoFocus-Stream/IL_AF_Stream.thy` (diff)
The file was modified	`thys/AutoFocus-Stream/ListSlice.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Digraph_Basic.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Misc.thy` (diff)
The file was modified	`thys/BDD/General.thy` (diff)
The file was modified	`thys/BDD/LevellistProof.thy` (diff)
The file was modified	`thys/BDD/NormalizeTotalProof.thy` (diff)
The file was modified	`thys/BDD/ProcedureSpecs.thy` (diff)
The file was modified	`thys/BDD/RepointProof.thy` (diff)
The file was modified	`thys/BDD/ShareRepProof.thy` (diff)
The file was modified	`thys/BinarySearchTree/BinaryTree.thy` (diff)
The file was modified	`thys/Binomial-Heaps/SkewBinomialHeap.thy` (diff)
The file was modified	`thys/Boolean_Expression_Checkers/Boolean_Expression_Checkers.thy` (diff)
The file was modified	`thys/Boolean_Expression_Checkers/Boolean_Expression_Checkers_AList_Mapping.thy` (diff)
The file was modified	`thys/Boolean_Expression_Checkers/Boolean_Expression_Example.thy` (diff)
The file was modified	`thys/Bounded_Deducibility_Security/BD_Security.thy` (diff)
The file was modified	`thys/Bounded_Deducibility_Security/Bounded_Deducibility_Security.thy` (diff)
The file was modified	`thys/Bounded_Deducibility_Security/Compositional_Reasoning.thy` (diff)
The file was modified	`thys/Bounded_Deducibility_Security/Trivia.thy` (diff)
The file was modified	`thys/BytecodeLogicJmlTypes/AssocLists.thy` (diff)
The file was modified	`thys/BytecodeLogicJmlTypes/Cachera.thy` (diff)
The file was modified	`thys/BytecodeLogicJmlTypes/Language.thy` (diff)
The file was modified	`thys/BytecodeLogicJmlTypes/Sound.thy` (diff)
The file was modified	`thys/CAVA_Automata/Automata.thy` (diff)
The file was modified	`thys/CAVA_Automata/Automata_Impl.thy` (diff)
The file was modified	`thys/CAVA_Automata/CAVA_Base/Lexord_List.thy` (diff)
The file was modified	`thys/CAVA_Automata/Digraph_Impl.thy` (diff)
The file was modified	`thys/CAVA_Automata/Lasso.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/BoolProgs/BoolProgs.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/BoolProgs/Programs/BoolProgs_Philosophers.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/BoolProgs/Programs/BoolProgs_Simple.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/CAVA_Impl.thy` (diff)
The file was modified	`thys/CCS/Strong_Sim_Pres.thy` (diff)
The file was modified	`thys/CCS/Weak_Cong_Semantics.thy` (diff)
The file was modified	`thys/CCS/Weak_Cong_Sim.thy` (diff)
The file was modified	`thys/CCS/Weak_Cong_Sim_Pres.thy` (diff)
The file was modified	`thys/CCS/Weak_Semantics.thy` (diff)
The file was modified	`thys/CCS/Weak_Sim.thy` (diff)
The file was modified	`thys/CCS/Weak_Sim_Pres.thy` (diff)
The file was modified	`thys/CISC-Kernel/trace/Rushby-with-Control/CISK.thy` (diff)
The file was modified	`thys/Card_Number_Partitions/Number_Partition.thy` (diff)
The file was modified	`thys/Card_Partitions/Card_Partitions.thy` (diff)
The file was modified	`thys/Case_Labeling/Case_Labeling_Examples.thy` (diff)
The file was modified	`thys/Case_Labeling/Examples/Conditionals.thy` (diff)
The file was modified	`thys/Cauchy/CauchysMeanTheorem.thy` (diff)
The file was modified	`thys/Cayley_Hamilton/Cayley_Hamilton.thy` (diff)
The file was modified	`thys/Cayley_Hamilton/Square_Matrix.thy` (diff)
The file was modified	`thys/Circus/Circus_Actions.thy` (diff)
The file was modified	`thys/Circus/Designs.thy` (diff)
The file was modified	`thys/Circus/Reactive_Processes.thy` (diff)
The file was modified	`thys/Circus/Refinement_Example.thy` (diff)
The file was modified	`thys/Circus/Relations.thy` (diff)
The file was modified	`thys/Circus/Var.thy` (diff)
The file was modified	`thys/Circus/Var_list.thy` (diff)
The file was modified	`thys/Coinductive/Coinductive_List.thy` (diff)
The file was modified	`thys/Coinductive/Coinductive_Nat.thy` (diff)
The file was modified	`thys/Coinductive/Coinductive_Stream.thy` (diff)
The file was modified	`thys/Coinductive/Complete_Partial_Order2.thy` (diff)
The file was modified	`thys/Coinductive/Examples/CCPO_Topology.thy` (diff)
The file was modified	`thys/Coinductive/Examples/Hamming_Stream.thy` (diff)
The file was modified	`thys/Coinductive/Examples/LList_CCPO_Topology.thy` (diff)
The file was modified	`thys/Coinductive/Examples/LMirror.thy` (diff)
The file was modified	`thys/Coinductive/Examples/TLList_CCPO_Examples.thy` (diff)
The file was modified	`thys/Coinductive/Lazy_TLList.thy` (diff)
The file was modified	`thys/Coinductive/Quotient_TLList.thy` (diff)
The file was modified	`thys/Coinductive/TLList.thy` (diff)
The file was modified	`thys/Coinductive/TLList_CCPO.thy` (diff)
The file was modified	`thys/Coinductive_Languages/Coinductive_Regular_Set.thy` (diff)
The file was modified	`thys/Collections/Collections_Entrypoints_Chapter.thy` (diff)
The file was modified	`thys/Collections/Examples/ICF/Exploration_DFS.thy` (diff)
The file was modified	`thys/Collections/GenCF/Gen/GenCF_Gen_Chapter.thy` (diff)
The file was modified	`thys/Collections/GenCF/GenCF_Chapter.thy` (diff)
The file was modified	`thys/Collections/GenCF/Impl/GenCF_Impl_Chapter.thy` (diff)
The file was modified	`thys/Collections/GenCF/Impl/Impl_Array_Hash_Map.thy` (diff)
The file was modified	`thys/Collections/GenCF/Impl/Impl_Array_Map.thy` (diff)
The file was modified	`thys/Collections/GenCF/Intf/GenCF_Intf_Chapter.thy` (diff)
The file was modified	`thys/Collections/GenCF/Intf/Intf_Comp.thy` (diff)
The file was modified	`thys/Collections/ICF/ICF_Autoref.thy` (diff)
The file was modified	`thys/Collections/ICF/ICF_Entrypoints_Chapter.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/Algos.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/ICF_Gen_Algo_Chapter.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/MapGA.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/SetGA.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/SetIndex.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/ArrayHashMap_Impl.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/HashMap_Impl.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/ICF_Impl_Chapter.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/Trie2.thy` (diff)
The file was modified	`thys/Collections/ICF/spec/ICF_Spec_Chapter.thy` (diff)
The file was modified	`thys/Collections/ICF/spec/MapSpec.thy` (diff)
The file was modified	`thys/Collections/Iterator/Idx_Iterator.thy` (diff)
The file was modified	`thys/Collections/Iterator/SetIteratorOperations.thy` (diff)
The file was modified	`thys/Collections/Lib/Assoc_List.thy` (diff)
The file was modified	`thys/Collections/Userguides/Userguides_Chapter.thy` (diff)
The file was modified	`thys/Completeness/Soundness.thy` (diff)
The file was modified	`thys/Consensus_Refined/Consensus_Misc.thy` (diff)
The file was modified	`thys/Consensus_Refined/Infra.thy` (diff)
The file was modified	`thys/Consensus_Refined/MRU/New_Algorithm_Proofs.thy` (diff)
The file was modified	`thys/Consensus_Refined/Voting/OneThirdRule_Proofs.thy` (diff)
The file was modified	`thys/Containers/AssocList.thy` (diff)
The file was modified	`thys/Containers/Closure_Set.thy` (diff)
The file was modified	`thys/Containers/Collection_Enum.thy` (diff)
The file was modified	`thys/Containers/Collection_Order.thy` (diff)
The file was modified	`thys/Containers/Containers.thy` (diff)
The file was modified	`thys/Containers/Containers_Auxiliary.thy` (diff)
The file was modified	`thys/Containers/Containers_Userguide.thy` (diff)
The file was modified	`thys/Containers/DList_Set.thy` (diff)
The file was modified	`thys/Containers/Equal.thy` (diff)
The file was modified	`thys/Containers/Extend_Partial_Order.thy` (diff)
The file was modified	`thys/Containers/ITP-2013/Benchmark_Bool.thy` (diff)
The file was modified	`thys/Containers/ITP-2013/Benchmark_Default.thy` (diff)
The file was modified	`thys/Containers/ITP-2013/Benchmark_ICF.thy` (diff)
The file was modified	`thys/Containers/ITP-2013/Benchmark_RBT.thy` (diff)
The file was modified	`thys/Containers/ITP-2013/Benchmark_Set.thy` (diff)
The file was modified	`thys/Containers/List_Fusion.thy` (diff)
The file was modified	`thys/Containers/List_Proper_Interval.thy` (diff)
The file was modified	`thys/Containers/Map_To_Mapping.thy` (diff)
The file was modified	`thys/Containers/Mapping_Impl.thy` (diff)
The file was modified	`thys/Containers/RBT_Mapping2.thy` (diff)
The file was modified	`thys/Containers/RBT_Set2.thy` (diff)
The file was modified	`thys/Containers/RBT_ext.thy` (diff)
The file was modified	`thys/Containers/Set_Impl.thy` (diff)
The file was modified	`thys/Containers/Set_Linorder.thy` (diff)
The file was modified	`thys/Containers/ccompare_generator.ML` (diff)
The file was modified	`thys/Containers/ceq_generator.ML` (diff)
The file was modified	`thys/CoreC++/Conform.thy` (diff)
The file was modified	`thys/CoreC++/Determinism.thy` (diff)
The file was modified	`thys/CoreC++/Equivalence.thy` (diff)
The file was modified	`thys/CoreC++/Exceptions.thy` (diff)
The file was modified	`thys/CoreC++/Execute.thy` (diff)
The file was modified	`thys/CoreC++/HeapExtension.thy` (diff)
The file was modified	`thys/CoreC++/Progress.thy` (diff)
The file was modified	`thys/CoreC++/SubObj.thy` (diff)
The file was modified	`thys/CoreC++/TypeSafe.thy` (diff)
The file was modified	`thys/CoreC++/WellForm.thy` (diff)
The file was modified	`thys/CoreC++/WellTypeRT.thy` (diff)
The file was modified	`thys/CryptoBasedCompositionalProperties/CompLocalSecrets.thy` (diff)
The file was modified	`thys/CryptoBasedCompositionalProperties/KnowledgeKeysSecrets.thy` (diff)
The file was modified	`thys/CryptoBasedCompositionalProperties/ListExtras.thy` (diff)
The file was modified	`thys/CryptoBasedCompositionalProperties/Secrecy.thy` (diff)
The file was modified	`thys/CryptoBasedCompositionalProperties/Secrecy_types.thy` (diff)
The file was modified	`thys/CryptoBasedCompositionalProperties/inout.thy` (diff)
The file was modified	`thys/DataRefinementIBP/DataRefinement.thy` (diff)
The file was modified	`thys/DataRefinementIBP/Statements.thy` (diff)
The file was modified	`thys/Datatype_Order_Generator/Derive_Aux.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Compiler.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Density_Contexts.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Semantics.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Target_Density_Contexts.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Target_Semantics.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Transformations.thy` (diff)
The file was modified	`thys/Derangements/Derangements.thy` (diff)
The file was modified	`thys/Deriving/Comparator_Generator/Comparator_Generator.thy` (diff)
The file was modified	`thys/Deriving/Comparator_Generator/Compare.thy` (diff)
The file was modified	`thys/Deriving/Comparator_Generator/Compare_Generator.thy` (diff)
The file was modified	`thys/Deriving/Comparator_Generator/Compare_Instances.thy` (diff)
The file was modified	`thys/Deriving/Comparator_Generator/Compare_Order_Instances.thy` (diff)
The file was modified	`thys/Deriving/Comparator_Generator/Compare_Rat.thy` (diff)
The file was modified	`thys/Deriving/Comparator_Generator/compare_code.ML` (diff)
The file was modified	`thys/Deriving/Comparator_Generator/compare_generator.ML` (diff)
The file was modified	`thys/Deriving/Derive_Examples.thy` (diff)
The file was modified	`thys/Deriving/Equality_Generator/Equality_Generator.thy` (diff)
The file was modified	`thys/Deriving/Equality_Generator/Equality_Instances.thy` (diff)
The file was modified	`thys/Deriving/Equality_Generator/equality_generator.ML` (diff)
The file was modified	`thys/Deriving/Generator_Aux.thy` (diff)
The file was modified	`thys/Deriving/Hash_Generator/Hash_Generator.thy` (diff)
The file was modified	`thys/Deriving/Hash_Generator/Hash_Instances.thy` (diff)
The file was modified	`thys/Deriving/Hash_Generator/hash_generator.ML` (diff)
The file was modified	`thys/Deriving/generator_aux.ML` (diff)
The file was modified	`thys/Descartes_Sign_Rule/Descartes_Sign_Rule.thy` (diff)
The file was modified	`thys/Dijkstra_Shortest_Path/Dijkstra.thy` (diff)
The file was modified	`thys/Dijkstra_Shortest_Path/GraphByMap.thy` (diff)
The file was modified	`thys/Discrete_Summation/Examples.thy` (diff)
The file was modified	`thys/DiskPaxos/DiskPaxos_Chosen.thy` (diff)
The file was modified	`thys/DiskPaxos/DiskPaxos_Inv1.thy` (diff)
The file was modified	`thys/DiskPaxos/DiskPaxos_Inv2.thy` (diff)
The file was modified	`thys/DiskPaxos/DiskPaxos_Inv3.thy` (diff)
The file was modified	`thys/DiskPaxos/DiskPaxos_Inv4.thy` (diff)
The file was modified	`thys/DiskPaxos/DiskPaxos_Inv5.thy` (diff)
The file was modified	`thys/DiskPaxos/DiskPaxos_Inv6.thy` (diff)
The file was modified	`thys/DiskPaxos/DiskPaxos_Model.thy` (diff)
The file was modified	`thys/Echelon_Form/Cayley_Hamilton_Compatible.thy` (diff)
The file was modified	`thys/Encodability_Process_Calculi/CombinedCriteria.thy` (diff)
The file was modified	`thys/Encodability_Process_Calculi/DivergenceReflection.thy` (diff)
The file was modified	`thys/Encodability_Process_Calculi/Encodings.thy` (diff)
The file was modified	`thys/Encodability_Process_Calculi/FullAbstraction.thy` (diff)
The file was modified	`thys/Encodability_Process_Calculi/ProcessCalculi.thy` (diff)
The file was modified	`thys/Encodability_Process_Calculi/Relations.thy` (diff)
The file was modified	`thys/Encodability_Process_Calculi/SimulationRelations.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Fekete.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Measure_Preserving_Transformations.thy` (diff)
The file was modified	`thys/Euler_Partition/Euler_Partition.thy` (diff)
The file was modified	`thys/FeatherweightJava/Execute.thy` (diff)
The file was modified	`thys/Featherweight_OCL/src/UML_Contracts.thy` (diff)
The file was modified	`thys/Featherweight_OCL/src/UML_Logic.thy` (diff)
The file was modified	`thys/Featherweight_OCL/src/UML_PropertyProfiles.thy` (diff)
The file was modified	`thys/Featherweight_OCL/src/UML_State.thy` (diff)
The file was modified	`thys/Featherweight_OCL/src/collection_types/UML_Bag.thy` (diff)
The file was modified	`thys/Featherweight_OCL/src/collection_types/UML_Sequence.thy` (diff)
The file was modified	`thys/Featherweight_OCL/src/collection_types/UML_Set.thy` (diff)
The file was modified	`thys/FileRefinement/CArrays.thy` (diff)
The file was modified	`thys/FinFun/Card_Univ.thy` (diff)
The file was modified	`thys/FinFun/FinFun.thy` (diff)
The file was modified	`thys/FinFun/FinFunPred.thy` (diff)
The file was modified	`thys/Finger-Trees/FingerTree.thy` (diff)
The file was modified	`thys/Finite_Automata_HF/Finite_Automata_HF.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/EnumeratorProps.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/FaceDivisionProps.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/GeneratorProps.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/GraphProps.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/Invariants.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/ListAux.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/Maps.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/Plane1Props.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/PlaneGraphIso.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/PlaneProps.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/ScoreProps.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/TameEnum.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/TameProps.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/Worklist.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/ArithExtras.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/BitBoolTS.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/FR.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/FR_proof.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/FR_types.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/Gateway.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/Gateway_proof.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/Gateway_proof_aux.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/Gateway_types.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/JoinSplitTime.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/ListExtras.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/SteamBoiler.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/SteamBoiler_proof.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/arith_hints.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/stream.thy` (diff)
The file was modified	`thys/Formal_SSA/Construct_SSA.thy` (diff)
The file was modified	`thys/Formal_SSA/Construct_SSA_code.thy` (diff)
The file was modified	`thys/Formal_SSA/Construct_SSA_notriv.thy` (diff)
The file was modified	`thys/Formal_SSA/Construct_SSA_notriv_code.thy` (diff)
The file was modified	`thys/Formal_SSA/Disjoin_Transform.thy` (diff)
The file was modified	`thys/Formal_SSA/FormalSSA_Misc.thy` (diff)
The file was modified	`thys/Formal_SSA/Graph_path.thy` (diff)
The file was modified	`thys/Formal_SSA/RBT_Mapping_Exts.thy` (diff)
The file was modified	`thys/Formal_SSA/SSA_Transfer_Rules.thy` (diff)
The file was modified	`thys/Formal_SSA/Serial_Rel.thy` (diff)
The file was modified	`thys/Formal_SSA/While_Combinator_Exts.thy` (diff)
The file was modified	`thys/Formula_Derivatives/Presburger_Examples.thy` (diff)
The file was modified	`thys/Formula_Derivatives/WS1S_Nameful.thy` (diff)
The file was modified	`thys/Formula_Derivatives/WS1S_Nameful_Examples.thy` (diff)
The file was modified	`thys/Formula_Derivatives/WS1S_Prelim.thy` (diff)
The file was modified	`thys/Formula_Derivatives/WS1S_Presburger_Equivalence.thy` (diff)
The file was modified	`thys/Free-Groups/Cancelation.thy` (diff)
The file was modified	`thys/Free-Groups/Generators.thy` (diff)
The file was modified	`thys/Free-Groups/UnitGroup.thy` (diff)
The file was modified	`thys/Functional-Automata/MaxChop.thy` (diff)
The file was modified	`thys/Functional-Automata/MaxPrefix.thy` (diff)
The file was modified	`thys/Gabow_SCC/Find_Path_Impl.thy` (diff)
The file was modified	`thys/Gabow_SCC/Gabow_GBG.thy` (diff)
The file was modified	`thys/Gabow_SCC/Gabow_Skeleton.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Elementary_Operations.thy` (diff)
The file was modified	`thys/Girth_Chromatic/Girth_Chromatic.thy` (diff)
The file was modified	`thys/Girth_Chromatic/Ugraphs.thy` (diff)
The file was modified	`thys/GoedelGod/GoedelGod.thy` (diff)
The file was modified	`thys/GraphMarkingIBP/Graph.thy` (diff)
The file was modified	`thys/GraphMarkingIBP/LinkMark.thy` (diff)
The file was modified	`thys/GraphMarkingIBP/StackMark.thy` (diff)
The file was modified	`thys/Graph_Theory/Bidirected_Digraph.thy` (diff)
The file was modified	`thys/Graph_Theory/Euler.thy` (diff)
The file was modified	`thys/Graph_Theory/Graph_Theory.thy` (diff)
The file was modified	`thys/Graph_Theory/Kuratowski.thy` (diff)
The file was modified	`thys/Graph_Theory/Shortest_Path.thy` (diff)
The file was modified	`thys/Graph_Theory/Weighted_Graph.thy` (diff)
The file was modified	`thys/HRB-Slicing/HRBSlicing.thy` (diff)
The file was modified	`thys/HRB-Slicing/JinjaVM_Inter/JVMCFG.thy` (diff)
The file was modified	`thys/HRB-Slicing/JinjaVM_Inter/JVMInterpretation.thy` (diff)
The file was modified	`thys/HRB-Slicing/JinjaVM_Inter/JVMPostdomination.thy` (diff)
The file was modified	`thys/HRB-Slicing/Proc/Interpretation.thy` (diff)
The file was modified	`thys/HRB-Slicing/Proc/Labels.thy` (diff)
The file was modified	`thys/HRB-Slicing/Proc/ProcSDG.thy` (diff)
The file was modified	`thys/HRB-Slicing/Proc/ProcState.thy` (diff)
The file was modified	`thys/HRB-Slicing/Proc/WellFormed.thy` (diff)
The file was modified	`thys/HRB-Slicing/StaticInter/BasicDefs.thy` (diff)
The file was modified	`thys/HRB-Slicing/StaticInter/CFG.thy` (diff)
The file was modified	`thys/HRB-Slicing/StaticInter/CFGExit_wf.thy` (diff)
The file was modified	`thys/HRB-Slicing/StaticInter/HRBSlice.thy` (diff)
The file was modified	`thys/HRB-Slicing/StaticInter/Observable.thy` (diff)
The file was modified	`thys/HRB-Slicing/StaticInter/Postdomination.thy` (diff)
The file was modified	`thys/HRB-Slicing/StaticInter/SCDObservable.thy` (diff)
The file was modified	`thys/HRB-Slicing/StaticInter/SemanticsCFG.thy` (diff)
The file was modified	`thys/HRB-Slicing/StaticInter/Slice.thy` (diff)
The file was modified	`thys/HRB-Slicing/StaticInter/WeakSimulation.thy` (diff)
The file was modified	`thys/Heard_Of/HOModel.thy` (diff)
The file was modified	`thys/Heard_Of/Reduction.thy` (diff)
The file was modified	`thys/HereditarilyFinite/Ordinal.thy` (diff)
The file was modified	`thys/Hermite/Hermite_IArrays.thy` (diff)
The file was modified	`thys/HotelKeyCards/Basis.thy` (diff)
The file was modified	`thys/HotelKeyCards/Equivalence.thy` (diff)
The file was modified	`thys/HotelKeyCards/NewCard.thy` (diff)
The file was modified	`thys/HotelKeyCards/State.thy` (diff)
The file was modified	`thys/HotelKeyCards/Trace.thy` (diff)
The file was modified	`thys/IEEE_Floating_Point/FloatProperty.thy` (diff)
The file was modified	`thys/Impossible_Geometry/Impossible_Geometry.thy` (diff)
The file was modified	`thys/Inductive_Confidentiality/DolevYao/Message.thy` (diff)
The file was modified	`thys/Inductive_Confidentiality/GeneralAttacker/MessageGA.thy` (diff)
The file was modified	`thys/Inductive_Confidentiality/GeneralAttacker/NS_Public_Bad_GA.thy` (diff)
The file was modified	`thys/InformationFlowSlicing/LiftingIntra.thy` (diff)
The file was modified	`thys/InformationFlowSlicing/NonInterferenceWhile.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/isabelle_home/src/HOL/Isabelle_Main0.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/isabelle_home/src/HOL/Isabelle_Main1.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/isabelle_home/src/HOL/Isabelle_Main2.thy` (diff)
The file was modified	`thys/Jinja/BV/BVExample.thy` (diff)
The file was modified	`thys/Jinja/BV/BVSpecTypeSafe.thy` (diff)
The file was modified	`thys/Jinja/BV/EffectMono.thy` (diff)
The file was modified	`thys/Jinja/BV/SemiType.thy` (diff)
The file was modified	`thys/Jinja/BV/TF_JVM.thy` (diff)
The file was modified	`thys/Jinja/Common/Objects.thy` (diff)
The file was modified	`thys/Jinja/Common/TypeRel.thy` (diff)
The file was modified	`thys/Jinja/Compiler/Correctness1.thy` (diff)
The file was modified	`thys/Jinja/Compiler/Correctness2.thy` (diff)
The file was modified	`thys/Jinja/Compiler/Hidden.thy` (diff)
The file was modified	`thys/Jinja/Compiler/TypeComp.thy` (diff)
The file was modified	`thys/Jinja/DFA/Abstract_BV.thy` (diff)
The file was modified	`thys/Jinja/DFA/Kildall.thy` (diff)
The file was modified	`thys/Jinja/DFA/LBVComplete.thy` (diff)
The file was modified	`thys/Jinja/DFA/LBVCorrect.thy` (diff)
The file was modified	`thys/Jinja/DFA/LBVSpec.thy` (diff)
The file was modified	`thys/Jinja/DFA/Typing_Framework_err.thy` (diff)
The file was modified	`thys/Jinja/J/Annotate.thy` (diff)
The file was modified	`thys/Jinja/J/BigStep.thy` (diff)
The file was modified	`thys/Jinja/J/Examples.thy` (diff)
The file was modified	`thys/Jinja/J/TypeSafe.thy` (diff)
The file was modified	`thys/Jinja/J/execute_WellType.thy` (diff)
The file was modified	`thys/Jinja/JVM/JVMDefensive.thy` (diff)
The file was modified	`thys/JinjaThreads/BV/BCVExec.thy` (diff)
The file was modified	`thys/JinjaThreads/BV/BVConform.thy` (diff)
The file was modified	`thys/JinjaThreads/BV/BVNoTypeError.thy` (diff)
The file was modified	`thys/JinjaThreads/BV/BVProgressThreaded.thy` (diff)
The file was modified	`thys/JinjaThreads/BV/BVSpecTypeSafe.thy` (diff)
The file was modified	`thys/JinjaThreads/BV/EffectMono.thy` (diff)
The file was modified	`thys/JinjaThreads/BV/JVMDeadlocked.thy` (diff)
The file was modified	`thys/JinjaThreads/BV/TF_JVM.thy` (diff)
The file was modified	`thys/JinjaThreads/Basic/Auxiliary.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/BinOp.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/Conform.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/ConformThreaded.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/ExternalCall.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/ExternalCallWF.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/SemiType.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/StartConfig.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/TypeRel.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/CallExpr.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/Compiler.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/Correctness.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/Correctness1.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/Correctness1Threaded.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/Correctness2.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/Exception_Tables.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/Execs.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J0.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J0Bisim.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J0J1Bisim.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J1.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J1Deadlock.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J1JVM.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J1JVMBisim.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J1State.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J1WellType.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/JJ1WellForm.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/JVMJ1.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/JVMTau.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/ListIndex.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/PCompiler.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/Preprocessor.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/TypeComp.thy` (diff)
The file was modified	`thys/JinjaThreads/DFA/Abstract_BV.thy` (diff)
The file was modified	`thys/JinjaThreads/DFA/LBVComplete.thy` (diff)
The file was modified	`thys/JinjaThreads/DFA/LBVCorrect.thy` (diff)
The file was modified	`thys/JinjaThreads/DFA/LBVSpec.thy` (diff)
The file was modified	`thys/JinjaThreads/DFA/Typing_Framework_err.thy` (diff)
The file was modified	`thys/JinjaThreads/Examples/ApprenticeChallenge.thy` (diff)
The file was modified	`thys/JinjaThreads/Examples/Examples_Main.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/Code_Generation.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/ExternalCall_Execute.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/JVMExec_Execute.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/JVMExec_Execute2.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/JVM_Execute2.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/J_Execute.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/Java2Jinja.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/PCompilerRefine.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/Random_Scheduler.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/Round_Robin.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/SC_Schedulers.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/Scheduler.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/State_Refinement.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/ToString.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/TypeRelRefine.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWBisimDeadlock.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWBisimulation.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWDeadlock.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWInterrupt.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWLTS.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWLifting.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWLiftingSem.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWLock.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWProgress.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWProgressAux.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWSemantics.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWThread.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWWait.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWWellform.thy` (diff)
The file was modified	`thys/JinjaThreads/J/DefAss.thy` (diff)
The file was modified	`thys/JinjaThreads/J/DefAssPreservation.thy` (diff)
The file was modified	`thys/JinjaThreads/J/Expr.thy` (diff)
The file was modified	`thys/JinjaThreads/J/JHeap.thy` (diff)
The file was modified	`thys/JinjaThreads/J/ProgressThreaded.thy` (diff)
The file was modified	`thys/JinjaThreads/J/SmallStep.thy` (diff)
The file was modified	`thys/JinjaThreads/J/Threaded.thy` (diff)
The file was modified	`thys/JinjaThreads/J/TypeSafe.thy` (diff)
The file was modified	`thys/JinjaThreads/J/WellType.thy` (diff)
The file was modified	`thys/JinjaThreads/J/WellTypeRT.thy` (diff)
The file was modified	`thys/JinjaThreads/JVM/JVMDefensive.thy` (diff)
The file was modified	`thys/JinjaThreads/JVM/JVMExceptions.thy` (diff)
The file was modified	`thys/JinjaThreads/JVM/JVMExecInstr.thy` (diff)
The file was modified	`thys/JinjaThreads/JVM/JVMHeap.thy` (diff)
The file was modified	`thys/JinjaThreads/JVM/JVMThreaded.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/DRF_J.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/DRF_JVM.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/HB_Completion.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Common.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Compiler_Type2.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Framework.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Heap.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_JVM_Typesafe.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_J_Typesafe.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Spec.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Type.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Type2.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Typesafe.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Typesafe2.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/Non_Speculative.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/SC.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/SC_Collections.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/SC_Completion.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/SC_Interp.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/SC_Legal.thy` (diff)
The file was modified	`thys/JiveDataStoreModel/Isabelle_Store/Store.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Char_Poly.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Column_Operations.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Conjugate.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gauss_Jordan.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gram_Schmidt.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form_Existence.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form_Uniqueness.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Comparison.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Complexity.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_IArray_Impl.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Impl.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Kernel.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Missing_Fraction_Field.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Missing_Permutations.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Missing_Ring.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Ring_Hom_Matrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Schur_Decomposition.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Show_Matrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Spectral_Radius.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/VS_Connect.thy` (diff)
The file was modified	`thys/KAT_and_DRA/SingleSorted/KAT.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Aux/AList_Mapping2.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Aux/List2.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Aux/Map2.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Aux/Mapping2.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Aux/Preliminaries2.thy` (diff)
The file was modified	`thys/LTL_to_DRA/DTS.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Impl/Export_Code.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Impl/LTL_CAVA_Compat.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Impl/LTL_Rabin_Impl.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Impl/Mojmir_Rabin_Impl.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Impl/af_Impl.thy` (diff)
The file was modified	`thys/LTL_to_DRA/LTL.thy` (diff)
The file was modified	`thys/LTL_to_DRA/LTL_Rabin.thy` (diff)
The file was modified	`thys/LTL_to_DRA/LTL_Rabin_Unfold_Opt.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Mojmir.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Mojmir_Rabin.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Rabin.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Semi_Mojmir.thy` (diff)
The file was modified	`thys/LTL_to_DRA/af.thy` (diff)
The file was modified	`thys/Landau_Symbols/Group_Sort.thy` (diff)
The file was modified	`thys/Landau_Symbols/Landau_Library.thy` (diff)
The file was modified	`thys/Landau_Symbols/Landau_Real_Products.thy` (diff)
The file was modified	`thys/Landau_Symbols/Landau_Simprocs.thy` (diff)
The file was modified	`thys/Landau_Symbols/Landau_Symbols.thy` (diff)
The file was modified	`thys/Landau_Symbols/Landau_Symbols_Definition.thy` (diff)
The file was modified	`thys/Landau_Symbols/landau_simprocs.ML` (diff)
The file was modified	`thys/LatticeProperties/Lattice_Prop.thy` (diff)
The file was modified	`thys/LatticeProperties/Modular_Distrib_Lattice.thy` (diff)
The file was modified	`thys/LightweightJava/Lightweight_Java_Equivalence.thy` (diff)
The file was modified	`thys/LightweightJava/Lightweight_Java_Proof.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/CertDlo.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/CertLin.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/Cooper.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/Logic.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/QE.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/QEdlo.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/QEdlo_fr.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/QEdlo_inf.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/QElin_inf.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/QEpres.thy` (diff)
The file was modified	`thys/List-Index/List_Index.thy` (diff)
The file was modified	`thys/List-Infinite/CommonArith/Util_Div.thy` (diff)
The file was modified	`thys/List-Infinite/CommonArith/Util_MinMax.thy` (diff)
The file was modified	`thys/List-Infinite/CommonArith/Util_NatInf.thy` (diff)
The file was modified	`thys/List-Infinite/CommonSet/SetInterval2.thy` (diff)
The file was modified	`thys/List-Infinite/CommonSet/SetIntervalCut.thy` (diff)
The file was modified	`thys/List-Infinite/CommonSet/SetIntervalStep.thy` (diff)
The file was modified	`thys/List-Infinite/ListInf/List2.thy` (diff)
The file was modified	`thys/List-Infinite/ListInf/ListInf.thy` (diff)
The file was modified	`thys/List-Infinite/ListInf/ListInf_Prefix.thy` (diff)
The file was modified	`thys/List-Infinite/ListInfinite.thy` (diff)
The file was modified	`thys/List_Update/BIT_2comp_on2.thy` (diff)
The file was modified	`thys/List_Update/Comb.thy` (diff)
The file was modified	`thys/List_Update/Competitive_Analysis.thy` (diff)
The file was modified	`thys/List_Update/List_Factoring.thy` (diff)
The file was modified	`thys/List_Update/On_Off.thy` (diff)
The file was modified	`thys/List_Update/Partial_Cost_Model.thy` (diff)
The file was modified	`thys/List_Update/Phase_Partitioning.thy` (diff)
The file was modified	`thys/List_Update/RExp_Var.thy` (diff)
The file was modified	`thys/Locally-Nameless-Sigma/Sigma/Sigma.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Formula.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/M2L.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Pi_Equivalence_Checking.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/WS1S.thy` (diff)
The file was modified	`thys/Markov_Models/Classifying_Markov_Chain_States.thy` (diff)
The file was modified	`thys/Markov_Models/Discrete_Time_Markov_Chain.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Crowds_Protocol.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Gossip_Broadcast.thy` (diff)
The file was modified	`thys/Markov_Models/ex/MDP_RP_Certification.thy` (diff)
The file was modified	`thys/Markov_Models/ex/PCTL.thy` (diff)
The file was modified	`thys/Markov_Models/ex/PGCL.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Zeroconf_Analysis.thy` (diff)
The file was modified	`thys/Marriage/Marriage.thy` (diff)
The file was modified	`thys/MonoBoolTranAlgebra/Assertion_Algebra.thy` (diff)
The file was modified	`thys/Myhill-Nerode/Closures.thy` (diff)
The file was modified	`thys/Myhill-Nerode/Folds.thy` (diff)
The file was modified	`thys/Myhill-Nerode/Myhill.thy` (diff)
The file was modified	`thys/Nat-Interval-Logic/IL_Interval.thy` (diff)
The file was modified	`thys/Nat-Interval-Logic/IL_IntervalOperators.thy` (diff)
The file was modified	`thys/Nat-Interval-Logic/IL_TemporalOperators.thy` (diff)
The file was modified	`thys/Native_Word/More_Bits_Int.thy` (diff)
The file was modified	`thys/Native_Word/Native_Cast.thy` (diff)
The file was modified	`thys/Native_Word/Uint8.thy` (diff)
The file was modified	`thys/Native_Word/Word_Misc.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Composition_Theory.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Impl.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Stateful_Policy_Algorithm.thy` (diff)
The file was modified	`thys/Nominal2/Nominal2_FCB.thy` (diff)
The file was modified	`thys/Nominal2/nominal_basics.ML` (diff)
The file was modified	`thys/Nominal2/nominal_dt_data.ML` (diff)
The file was modified	`thys/NormByEval/NBE.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Library/Higher_Derivative.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Library/Multivariate_Taylor.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Euler_Affine.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ordinary_Differential_Equations.thy` (diff)
The file was modified	`thys/PCF/Continuations.thy` (diff)
The file was modified	`thys/POPLmark-deBruijn/Basis.thy` (diff)
The file was modified	`thys/POPLmark-deBruijn/Execute.thy` (diff)
The file was modified	`thys/POPLmark-deBruijn/POPLmarkRecord.thy` (diff)
The file was modified	`thys/Parity_Game/Strategy.thy` (diff)
The file was modified	`thys/Perfect-Number-Thm/Perfect.thy` (diff)
The file was modified	`thys/Perfect-Number-Thm/PerfectBasics.thy` (diff)
The file was modified	`thys/Perfect-Number-Thm/Sigma.thy` (diff)
The file was modified	`thys/Pi_Calculus/Agent.thy` (diff)
The file was modified	`thys/Pi_Calculus/Early_Semantics.thy` (diff)
The file was modified	`thys/Pi_Calculus/Early_Tau_Chain.thy` (diff)
The file was modified	`thys/Pi_Calculus/Late_Hennessy.thy` (diff)
The file was modified	`thys/Pi_Calculus/Rel.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Early_Bisim_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Early_Bisim_Subst.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Early_Bisim_Subst_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Early_Late_Comp.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Early_Sim.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Late_Axiomatisation.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Late_Bisim.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Late_Bisim_SC.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Late_Bisim_Subst.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Late_Bisim_Subst_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Late_Expansion_Law.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Late_Sim.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Late_Sim_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Strong_Late_Sim_bak.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Bisim_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Bisim_SC.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Bisim_Subst.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Bisim_Subst_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Bisim_Subst_SC.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Cong.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Cong_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Cong_SC.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Cong_Subst_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Cong_Subst_SC.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Late_Comp.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Semantics.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Sim.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Sim_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Step_Semantics.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Step_Sim_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Bisim.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Bisim_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Bisim_Subst.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Bisim_Subst_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Bisim_Subst_SC.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Cong.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Cong_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Cong_Subst_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Cong_Subst_SC.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Semantics.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Sim.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Sim_Pres.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Step_Semantics.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Step_Sim.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Late_Step_Sim_Pres.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Digraph_Map_Impl.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Full.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Planar_Complete.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Planar_Subdivision.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Planar_Subgraph.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Verification/Check_Non_Planarity_Verification.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Verification/Setup_AutoCorres.thy` (diff)
The file was modified	`thys/Planarity_Certificates/l4v/lib/OptionMonad.thy` (diff)
The file was modified	`thys/Planarity_Certificates/l4v/lib/OptionMonadND.thy` (diff)
The file was modified	`thys/Planarity_Certificates/l4v/lib/OptionMonadWP.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Explicit_Roots.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Factorization_Oracle.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Gauss_Jordan_Field.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Hybrid_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Missing_List.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Missing_Multiset.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Polynomial_Divisibility.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Polynomial_Field.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Precomputation.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Rational_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Rational_Root_Test.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Select_Berlekamp_Hensel_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Select_External_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Select_Hybrid_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Unsorted.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Neville_Aitken_Interpolation.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Polynomial_Interpolation.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom.thy` (diff)
The file was modified	`thys/Possibilistic_Noninterference/After_Execution.thy` (diff)
The file was modified	`thys/Possibilistic_Noninterference/MyTactics.thy` (diff)
The file was modified	`thys/Possibilistic_Noninterference/Syntactic_Criteria.thy` (diff)
The file was modified	`thys/Prime_Harmonic_Series/Prime_Harmonic.thy` (diff)
The file was modified	`thys/Prime_Harmonic_Series/Prime_Harmonic_Misc.thy` (diff)
The file was modified	`thys/Prime_Harmonic_Series/Squarefree_Nat.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Syntactic_Criteria.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Trace_Based.thy` (diff)
The file was modified	`thys/Probabilistic_System_Zoo/Vardi.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/AcquisitionHistory.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/ConsInterleave.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Misc.thy` (diff)
The file was modified	`thys/Promela/PromelaAST.thy` (diff)
The file was modified	`thys/Promela/PromelaInvariants.thy` (diff)
The file was modified	`thys/Promela/PromelaLTLConv.thy` (diff)
The file was modified	`thys/PseudoHoops/LeftComplementedMonoid.thy` (diff)
The file was modified	`thys/PseudoHoops/Operations.thy` (diff)
The file was modified	`thys/PseudoHoops/SpecialPseudoHoops.thy` (diff)
The file was modified	`thys/Psi_Calculi/Agent.thy` (diff)
The file was modified	`thys/Psi_Calculi/Semantics.thy` (diff)
The file was modified	`thys/Psi_Calculi/Sim_Struct_Cong.thy` (diff)
The file was modified	`thys/Psi_Calculi/Structural_Congruence.thy` (diff)
The file was modified	`thys/Psi_Calculi/Subst_Term.thy` (diff)
The file was modified	`thys/Psi_Calculi/Tau.thy` (diff)
The file was modified	`thys/Psi_Calculi/Tau_Laws_No_Weak.thy` (diff)
The file was modified	`thys/Psi_Calculi/Tau_Sim.thy` (diff)
The file was modified	`thys/Psi_Calculi/Tau_Stat_Imp.thy` (diff)
The file was modified	`thys/Psi_Calculi/Weak_Bisim_Pres.thy` (diff)
The file was modified	`thys/Psi_Calculi/Weak_Bisimulation.thy` (diff)
The file was modified	`thys/Psi_Calculi/Weak_Cong_Pres.thy` (diff)
The file was modified	`thys/Psi_Calculi/Weak_Cong_Sim_Pres.thy` (diff)
The file was modified	`thys/Psi_Calculi/Weak_Cong_Struct_Cong.thy` (diff)
The file was modified	`thys/Psi_Calculi/Weak_Stat_Imp.thy` (diff)
The file was modified	`thys/Psi_Calculi/Weak_Stat_Imp_Pres.thy` (diff)
The file was modified	`thys/Psi_Calculi/Weaken_Simulation.thy` (diff)
The file was modified	`thys/Psi_Calculi/Weaken_Stat_Imp.thy` (diff)
The file was modified	`thys/Psi_Calculi/Weaken_Transition.thy` (diff)
The file was modified	`thys/QR_Decomposition/Generalizations2.thy` (diff)
The file was modified	`thys/QR_Decomposition/Projections.thy` (diff)
The file was modified	`thys/QR_Decomposition/QR_Efficient.thy` (diff)
The file was modified	`thys/RIPEMD-160-SPARK/RIPEMD_160_SPARK.thy` (diff)
The file was modified	`thys/RSAPSS/Word.thy` (diff)
The file was modified	`thys/Real_Impl/Real_Unique_Impl.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/CPair.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/PRecFinSet.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/PRecFun.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/PRecList.thy` (diff)
The file was modified	`thys/Refine_Monadic/Generic/RefineG_While.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_Basic.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_Det.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_Misc.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_While.thy` (diff)
The file was modified	`thys/Regular-Sets/Derivatives.thy` (diff)
The file was modified	`thys/Regular-Sets/Equivalence_Checking2.thy` (diff)
The file was modified	`thys/Regular-Sets/Regular_Exp.thy` (diff)
The file was modified	`thys/Regular_Algebras/Dioid_Power_Sum.thy` (diff)
The file was modified	`thys/Regular_Algebras/Pratts_Counterexamples.thy` (diff)
The file was modified	`thys/Regular_Algebras/Regular_Algebra_Models.thy` (diff)
The file was modified	`thys/Regular_Algebras/Regular_Algebra_Variants.thy` (diff)
The file was modified	`thys/Regular_Algebras/Regular_Algebras.thy` (diff)
The file was modified	`thys/Ribbon_Proofs/Ribbons_Basic.thy` (diff)
The file was modified	`thys/Ribbon_Proofs/Ribbons_Graphical.thy` (diff)
The file was modified	`thys/Ribbon_Proofs/Ribbons_Stratified.thy` (diff)
The file was modified	`thys/SATSolverVerification/AssertLiteral.thy` (diff)
The file was modified	`thys/SATSolverVerification/CNF.thy` (diff)
The file was modified	`thys/SATSolverVerification/ConflictAnalysis.thy` (diff)
The file was modified	`thys/SATSolverVerification/Decide.thy` (diff)
The file was modified	`thys/SATSolverVerification/FunctionalImplementation.thy` (diff)
The file was modified	`thys/SATSolverVerification/Initialization.thy` (diff)
The file was modified	`thys/SATSolverVerification/MoreList.thy` (diff)
The file was modified	`thys/SATSolverVerification/SatSolverCode.thy` (diff)
The file was modified	`thys/SATSolverVerification/SatSolverVerification.thy` (diff)
The file was modified	`thys/SATSolverVerification/SolveLoop.thy` (diff)
The file was modified	`thys/SATSolverVerification/Trail.thy` (diff)
The file was modified	`thys/SIFPL/ContextOBJ.thy` (diff)
The file was modified	`thys/SIFPL/ContextVS.thy` (diff)
The file was modified	`thys/SIFPL/Lattice.thy` (diff)
The file was modified	`thys/SIFPL/PBIJ.thy` (diff)
The file was modified	`thys/SIFUM_Type_Systems/Language.thy` (diff)
The file was modified	`thys/SIFUM_Type_Systems/LocallySoundModeUse.thy` (diff)
The file was modified	`thys/Selection_Heap_Sort/Heap.thy` (diff)
The file was modified	`thys/Selection_Heap_Sort/SelectionSort_Functional.thy` (diff)
The file was modified	`thys/SenSocialChoice/May.thy` (diff)
The file was modified	`thys/Separation_Algebra/Map_Extra.thy` (diff)
The file was modified	`thys/Separation_Algebra/ex/capDL/Abstract_Separation_D.thy` (diff)
The file was modified	`thys/Separation_Algebra/ex/capDL/Separation_D.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Automation.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Examples/Array_Map_Impl.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Examples/Array_Set_Impl.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Examples/Imp_Set_Spec.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Examples/List_Seg.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Examples/Union_Find.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Hoare_Triple.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Run.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Tools/Sep_Misc.thy` (diff)
The file was modified	`thys/SequentInvertibility/MultiSequents.thy` (diff)
The file was modified	`thys/SequentInvertibility/NominalSequents.thy` (diff)
The file was modified	`thys/SequentInvertibility/SingleSuccedent.thy` (diff)
The file was modified	`thys/Show/Show_Real.thy` (diff)
The file was modified	`thys/Simpl/AlternativeSmallStep.thy` (diff)
The file was modified	`thys/Simpl/HeapList.thy` (diff)
The file was modified	`thys/Simpl/Hoare.thy` (diff)
The file was modified	`thys/Simpl/HoarePartial.thy` (diff)
The file was modified	`thys/Simpl/HoarePartialDef.thy` (diff)
The file was modified	`thys/Simpl/HoarePartialProps.thy` (diff)
The file was modified	`thys/Simpl/Language.thy` (diff)
The file was modified	`thys/Simpl/Semantic.thy` (diff)
The file was modified	`thys/Simpl/Simpl.thy` (diff)
The file was modified	`thys/Simpl/SmallStep.thy` (diff)
The file was modified	`thys/Simpl/StateSpace.thy` (diff)
The file was modified	`thys/Simpl/SyntaxTest.thy` (diff)
The file was modified	`thys/Simpl/Termination.thy` (diff)
The file was modified	`thys/Simpl/Vcg.thy` (diff)
The file was modified	`thys/Simpl/XVcg.thy` (diff)
The file was modified	`thys/Simpl/ex/Closure.thy` (diff)
The file was modified	`thys/Simpl/ex/ClosureEx.thy` (diff)
The file was modified	`thys/Simpl/ex/Quicksort.thy` (diff)
The file was modified	`thys/Simpl/ex/VcgEx.thy` (diff)
The file was modified	`thys/Simpl/ex/VcgExSP.thy` (diff)
The file was modified	`thys/Simpl/ex/VcgExTotal.thy` (diff)
The file was modified	`thys/Simpl/hoare.ML` (diff)
The file was modified	`thys/Slicing/Basic/CFGExit_wf.thy` (diff)
The file was modified	`thys/Slicing/Basic/DynStandardControlDependence.thy` (diff)
The file was modified	`thys/Slicing/Basic/DynWeakControlDependence.thy` (diff)
The file was modified	`thys/Slicing/Dynamic/DynSlice.thy` (diff)
The file was modified	`thys/Slicing/JinjaVM/JVMPostdomination.thy` (diff)
The file was modified	`thys/Slicing/JinjaVM/SemanticsWF.thy` (diff)
The file was modified	`thys/Slicing/StaticIntra/CDepInstantiations.thy` (diff)
The file was modified	`thys/Slicing/StaticIntra/PDG.thy` (diff)
The file was modified	`thys/Slicing/StaticIntra/Slice.thy` (diff)
The file was modified	`thys/Slicing/StaticIntra/StandardControlDependence.thy` (diff)
The file was modified	`thys/Slicing/StaticIntra/WeakControlDependence.thy` (diff)
The file was modified	`thys/Slicing/StaticIntra/WeakOrderDependence.thy` (diff)
The file was modified	`thys/Slicing/While/AdditionalLemmas.thy` (diff)
The file was modified	`thys/Slicing/While/DynamicControlDependences.thy` (diff)
The file was modified	`thys/Slicing/While/StaticControlDependences.thy` (diff)
The file was modified	`thys/Slicing/While/WellFormed.thy` (diff)
The file was modified	`thys/Statecharts/Contrib.thy` (diff)
The file was modified	`thys/Statecharts/Data.thy` (diff)
The file was modified	`thys/Statecharts/HAKripke.thy` (diff)
The file was modified	`thys/Statecharts/Kripke.thy` (diff)
The file was modified	`thys/Statecharts/SA.thy` (diff)
The file was modified	`thys/Statecharts/Update.thy` (diff)
The file was modified	`thys/Stern_Brocot/Cotree_Algebra.thy` (diff)
The file was modified	`thys/Strong_Security/Domain_example.thy` (diff)
The file was modified	`thys/Strong_Security/Strongly_Secure_Skip_Assign.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Lib/Misc_Polynomial.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Sturm_Method.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Sturm_Theorem.thy` (diff)
The file was modified	`thys/Tail_Recursive_Functions/CaseStudy2.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/Action.thy` (diff)
The file was modified	`thys/Transitive-Closure-II/RTrancl.thy` (diff)
The file was modified	`thys/Triangle/Angles.thy` (diff)
The file was modified	`thys/Triangle/Triangle.thy` (diff)
The file was modified	`thys/Trie/Trie.thy` (diff)
The file was modified	`thys/UPF/Monads.thy` (diff)
The file was modified	`thys/UPF/Normalisation.thy` (diff)
The file was modified	`thys/UPF/NormalisationTestSpecification.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Grid_Point.thy` (diff)
The file was modified	`thys/VectorSpace/LinearCombinations.thy` (diff)
The file was modified	`thys/VectorSpace/VectorSpace.thy` (diff)