Changes

Summary

merged
prefer plain subscript syntax;
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -d '$AFP' -a -x Sepref_Basic -x Sepref_IICF -x Iptables_Semantics_Examples_Big;
clarified parent session, in order to disentangle imports;
clarified imports;
clarified imports;
clarified imports;

Changeset 8192:0a57dd7e945a by wenzelm: merged
Changeset 8191:085877786e08 by wenzelm: prefer plain subscript syntax;
The file was modified	`thys/HRB-Slicing/StaticInter/HRBSlice.thy` (diff)
The file was modified	`thys/HRB-Slicing/StaticInter/SDG.thy` (diff)
The file was modified	`thys/HRB-Slicing/StaticInter/WeakSimulation.thy` (diff)
The file was modified	`thys/Slicing/Dynamic/DependentLiveVariables.thy` (diff)
The file was modified	`thys/Slicing/Dynamic/DynPDG.thy` (diff)
The file was modified	`thys/Slicing/Dynamic/DynSlice.thy` (diff)
The file was modified	`thys/Slicing/StaticIntra/CDepInstantiations.thy` (diff)
The file was modified	`thys/Slicing/StaticIntra/ControlDependenceRelations.thy` (diff)
The file was modified	`thys/Slicing/StaticIntra/PDG.thy` (diff)
The file was modified	`thys/Slicing/StaticIntra/WeakOrderDependence.thy` (diff)
Changeset 8190:d7b4f45e07a9 by wenzelm: session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks'  -d '$AFP' -a -x Sepref_Basic -x Sepref_IICF -x Iptables_Semantics_Examples_Big;
The file was modified	`thys/AODV/Aodv.thy` (diff)
The file was modified	`thys/AODV/Aodv_Basic.thy` (diff)
The file was modified	`thys/AODV/Aodv_Loop_Freedom.thy` (diff)
The file was modified	`thys/AODV/Global_Invariants.thy` (diff)
The file was modified	`thys/AODV/OAodv.thy` (diff)
The file was modified	`thys/AODV/Seq_Invariants.thy` (diff)
The file was modified	`thys/AODV/variants/a_norreqid/A_Aodv.thy` (diff)
The file was modified	`thys/AODV/variants/a_norreqid/A_Aodv_Loop_Freedom.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_OAodv.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.thy` (diff)
The file was modified	`thys/AODV/variants/b_fwdrreps/B_Aodv_Loop_Freedom.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_OAodv.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.thy` (diff)
The file was modified	`thys/AODV/variants/c_gtobcast/C_Aodv_Loop_Freedom.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_OAodv.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.thy` (diff)
The file was modified	`thys/AODV/variants/d_fwdrreqs/D_Aodv_Loop_Freedom.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_OAodv.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.thy` (diff)
The file was modified	`thys/AODV/variants/e_all_abcd/E_Aodv_Loop_Freedom.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_OAodv.thy` (diff)
The file was modified	`thys/AODV/variants/e_all_abcd/E_Seq_Invariants.thy` (diff)
The file was modified	`thys/Abs_Int_ITP2012/ACom.thy` (diff)
The file was modified	`thys/Abs_Int_ITP2012/Abs_Int0.thy` (diff)
The file was modified	`thys/Abs_Int_ITP2012/Abs_Int1_const.thy` (diff)
The file was modified	`thys/Abs_Int_ITP2012/Abs_Int2.thy` (diff)
The file was modified	`thys/Abs_Int_ITP2012/Abs_Int2_ivl.thy` (diff)
The file was modified	`thys/Abs_Int_ITP2012/Abs_State.thy` (diff)
The file was modified	`thys/Abs_Int_ITP2012/ROOT` (diff)
The file was modified	`thys/Abstract-Rewriting/Abstract_Rewriting.thy` (diff)
The file was modified	`thys/Abstract-Rewriting/ROOT` (diff)
The file was modified	`thys/Abstract-Rewriting/SN_Order_Carrier.thy` (diff)
The file was modified	`thys/Abstract-Rewriting/Seq.thy` (diff)
The file was modified	`thys/Abstract_Completeness/Abstract_Completeness.thy` (diff)
The file was modified	`thys/Abstract_Completeness/ROOT` (diff)
The file was modified	`thys/Abstract_Soundness/Finite_Proof_Soundness.thy` (diff)
The file was modified	`thys/Abstract_Soundness/Infinite_Proof_Soundness.thy` (diff)
The file was modified	`thys/Abstract_Soundness/ROOT` (diff)
The file was modified	`thys/Affine_Arithmetic/Affine_Approximation.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/Euclidean_Space_Explicit.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Executable_Euclidean_Space.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Float_Real.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/ROOT` (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_Real.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Master_Theorem.thy` (diff)
The file was modified	`thys/Akra_Bazzi/ROOT` (diff)
The file was modified	`thys/Algebraic_Numbers/Algebraic_Number_Tests.thy` (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/Bivariate_Polynomials.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Compare_Complex.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Complex_Roots_Real_Poly.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/ROOT` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Resultant.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Show_Real_Alg.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Show_Real_Approx.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Show_Real_Precise.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Sturm_Rat.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Unique_Factorization.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Unique_Factorization_Poly.thy` (diff)
The file was modified	`thys/Algebraic_VCs/AVC_KAD/Path_Model_Example.thy` (diff)
The file was modified	`thys/Algebraic_VCs/AVC_KAD/Pointer_Examples.thy` (diff)
The file was modified	`thys/Algebraic_VCs/AVC_KAD/VC_KAD.thy` (diff)
The file was modified	`thys/Algebraic_VCs/AVC_KAD/VC_KAD_Examples2.thy` (diff)
The file was modified	`thys/Algebraic_VCs/AVC_KAD/VC_KAD_wf.thy` (diff)
The file was modified	`thys/Algebraic_VCs/AVC_KAT/VC_KAT.thy` (diff)
The file was modified	`thys/Algebraic_VCs/AVC_KAT/VC_KAT_Examples2.thy` (diff)
The file was modified	`thys/Algebraic_VCs/Domain_Quantale.thy` (diff)
The file was modified	`thys/Algebraic_VCs/KAD_is_KAT.thy` (diff)
The file was modified	`thys/Algebraic_VCs/ROOT` (diff)
The file was modified	`thys/Allen_Calculus/allen.thy` (diff)
The file was modified	`thys/Allen_Calculus/nest.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Pairing_Heap_List1_Analysis.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Pairing_Heap_List2_Analysis.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Pairing_Heap_Tree_Analysis.thy` (diff)
The file was modified	`thys/Amortized_Complexity/ROOT` (diff)
The file was modified	`thys/Amortized_Complexity/Skew_Heap_Analysis.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Splay_Heap_Analysis.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Splay_Tree_Analysis_Base.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Splay_Tree_Analysis_Optimal.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Abstract_AF.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_DNEList.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_List.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Monoid.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Open_State.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_Probability_List.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/Applicative_Vector.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Beta_Eta.thy` (diff)
The file was modified	`thys/Applicative_Lifting/ROOT` (diff)
The file was modified	`thys/Applicative_Lifting/Tree_Relabelling.thy` (diff)
The file was modified	`thys/ArrowImpossibilityGS/Thys/Arrow_Order.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/Automatic_Refinement.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/Automatic_Refinement/Parametricity/Param_Tool.thy` (diff)
The file was modified	`thys/Automatic_Refinement/ROOT` (diff)
The file was modified	`thys/BDD/BinDag.thy` (diff)
The file was modified	`thys/BDD/LevellistProof.thy` (diff)
The file was modified	`thys/BDD/ProcedureSpecs.thy` (diff)
The file was modified	`thys/BDD/ShareRepProof.thy` (diff)
The file was modified	`thys/Bell_Numbers_Spivey/Bell_Numbers.thy` (diff)
The file was modified	`thys/Bell_Numbers_Spivey/ROOT` (diff)
The file was modified	`thys/Bell_Numbers_Spivey/Set_Partition.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Arithmetic_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Berlekamp_Zassenhaus.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Chinese_Remainder_Poly.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Code_Abort_Gcd.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Degree_Bound.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Distinct_Degree_Factorization.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Factor_Bound.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Factorization_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Hensel_Lifting.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Karatsuba_Multiplication.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Mahler_Measure.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Matrix_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Poly_Mod_Finite_Field.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/ROOT` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Reconstruction.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Square_Free_Int_To_Square_Free_GFp.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Sublist_Iteration.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Suitable_Prime.thy` (diff)
The file was modified	`thys/Bernoulli/Bernoulli_FPS.thy` (diff)
The file was modified	`thys/Bernoulli/Periodic_Bernpoly.thy` (diff)
The file was modified	`thys/Bertrands_Postulate/Bertrand.thy` (diff)
The file was modified	`thys/Bertrands_Postulate/ROOT` (diff)
The file was modified	`thys/Binomial-Heaps/BinomialHeap.thy` (diff)
The file was modified	`thys/Binomial-Heaps/SkewBinomialHeap.thy` (diff)
The file was modified	`thys/Binomial-Heaps/Test.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/Buildings/Algebra.thy` (diff)
The file was modified	`thys/CAVA_Automata/CAVA_Base/CAVA_Base.thy` (diff)
The file was modified	`thys/CAVA_Automata/CAVA_Base/CAVA_Code_Target.thy` (diff)
The file was modified	`thys/CAVA_Automata/CAVA_Base/Code_String.thy` (diff)
The file was modified	`thys/CAVA_Automata/Digraph.thy` (diff)
The file was modified	`thys/CAVA_Automata/Lasso.thy` (diff)
The file was modified	`thys/CAVA_Automata/ROOT` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/BoolProgs/BoolProgs.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/BoolProgs/BoolProgs_Extras.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/BoolProgs/BoolProgs_LTL_Conv.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/BoolProgs/Programs/BoolProgs_Programs.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/CAVA_Abstract.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/CAVA_Impl.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI_Statistics.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/ROOT` (diff)
The file was modified	`thys/CCS/Agent.thy` (diff)
The file was modified	`thys/CISC-Kernel/trace/Rushby-with-Control/K.thy` (diff)
The file was modified	`thys/CISC-Kernel/trace/Rushby-with-Control/List_Theorems.thy` (diff)
The file was modified	`thys/CISC-Kernel/trace/Rushby-with-Control/Option_Binders.thy` (diff)
The file was modified	`thys/CISC-Kernel/trace/Rushby-with-Control/Separation_kernel_model.thy` (diff)
The file was modified	`thys/CRDT/ROOT` (diff)
The file was modified	`thys/CRDT/Util.thy` (diff)
The file was modified	`thys/Call_Arity/AEnv.thy` (diff)
The file was modified	`thys/Call_Arity/AList-Utils-HOLCF.thy` (diff)
The file was modified	`thys/Call_Arity/AbstractTransform.thy` (diff)
The file was modified	`thys/Call_Arity/AnalBinds.thy` (diff)
The file was modified	`thys/Call_Arity/Arity-Nominal.thy` (diff)
The file was modified	`thys/Call_Arity/Arity.thy` (diff)
The file was modified	`thys/Call_Arity/ArityAnalysisCorrDenotational.thy` (diff)
The file was modified	`thys/Call_Arity/ArityAnalysisSig.thy` (diff)
The file was modified	`thys/Call_Arity/ArityAnalysisStack.thy` (diff)
The file was modified	`thys/Call_Arity/ArityStack.thy` (diff)
The file was modified	`thys/Call_Arity/Cardinality-Domain-Lists.thy` (diff)
The file was modified	`thys/Call_Arity/Cardinality-Domain.thy` (diff)
The file was modified	`thys/Call_Arity/CoCallAnalysisImpl.thy` (diff)
The file was modified	`thys/Call_Arity/CoCallAnalysisSig.thy` (diff)
The file was modified	`thys/Call_Arity/CoCallFix.thy` (diff)
The file was modified	`thys/Call_Arity/CoCallGraph-Nominal.thy` (diff)
The file was modified	`thys/Call_Arity/CoCallGraph.thy` (diff)
The file was modified	`thys/Call_Arity/Env-Set-Cpo.thy` (diff)
The file was modified	`thys/Call_Arity/EtaExpansion.thy` (diff)
The file was modified	`thys/Call_Arity/ROOT` (diff)
The file was modified	`thys/Call_Arity/SestoftConf.thy` (diff)
The file was modified	`thys/Call_Arity/SestoftCorrect.thy` (diff)
The file was modified	`thys/Call_Arity/Set-Cpo.thy` (diff)
The file was modified	`thys/Call_Arity/TTree-HOLCF.thy` (diff)
The file was modified	`thys/Call_Arity/TransformTools.thy` (diff)
The file was modified	`thys/Call_Arity/TrivialArityAnal.thy` (diff)
The file was modified	`thys/Card_Equiv_Relations/Card_Equiv_Relations.thy` (diff)
The file was modified	`thys/Card_Equiv_Relations/More_Set_Partition.thy` (diff)
The file was modified	`thys/Card_Equiv_Relations/ROOT` (diff)
The file was modified	`thys/Card_Multisets/Card_Multisets.thy` (diff)
The file was modified	`thys/Card_Number_Partitions/Additions_to_Main.thy` (diff)
The file was modified	`thys/Card_Partitions/Card_Partitions.thy` (diff)
The file was modified	`thys/Cartan_FP/Cartan.thy` (diff)
The file was modified	`thys/Case_Labeling/Examples/Conditionals.thy` (diff)
The file was modified	`thys/Case_Labeling/Examples/Hoare/Labeled_Hoare.thy` (diff)
The file was modified	`thys/Case_Labeling/Examples/Hoare/Labeled_Hoare_Examples.thy` (diff)
The file was modified	`thys/Case_Labeling/Examples/Monadic_Language.thy` (diff)
The file was modified	`thys/Case_Labeling/ROOT` (diff)
The file was modified	`thys/Catalan_Numbers/Catalan_Auxiliary_Integral.thy` (diff)
The file was modified	`thys/Catalan_Numbers/Catalan_Numbers.thy` (diff)
The file was modified	`thys/Catalan_Numbers/ROOT` (diff)
The file was modified	`thys/Category/Cat.thy` (diff)
The file was modified	`thys/Category2/Category.thy` (diff)
The file was modified	`thys/Category2/ROOT` (diff)
The file was modified	`thys/Category2/Universe.thy` (diff)
The file was modified	`thys/Category3/Category.thy` (diff)
The file was modified	`thys/Category3/Subcategory.thy` (diff)
The file was modified	`thys/Cayley_Hamilton/Cayley_Hamilton.thy` (diff)
The file was modified	`thys/Cayley_Hamilton/ROOT` (diff)
The file was modified	`thys/Cayley_Hamilton/Square_Matrix.thy` (diff)
The file was modified	`thys/Certification_Monads/Error_Monad.thy` (diff)
The file was modified	`thys/Certification_Monads/Error_Syntax.thy` (diff)
The file was modified	`thys/Certification_Monads/Parser_Monad.thy` (diff)
The file was modified	`thys/Certification_Monads/ROOT` (diff)
The file was modified	`thys/Certification_Monads/Strict_Sum.thy` (diff)
The file was modified	`thys/Chord_Segments/Chord_Segments.thy` (diff)
The file was modified	`thys/Chord_Segments/ROOT` (diff)
The file was modified	`thys/Circus/Circus_Actions.thy` (diff)
The file was modified	`thys/Circus/ROOT` (diff)
The file was modified	`thys/Circus/Reactive_Processes.thy` (diff)
The file was modified	`thys/CofGroups/CofGroups.thy` (diff)
The file was modified	`thys/Coinductive/Coinductive_List.thy` (diff)
The file was modified	`thys/Coinductive/Coinductive_List_Prefix.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/Examples/CCPO_Topology.thy` (diff)
The file was modified	`thys/Coinductive/Examples/Hamming_Stream.thy` (diff)
The file was modified	`thys/Coinductive/Examples/Resumption.thy` (diff)
The file was modified	`thys/Coinductive/Quotient_Coinductive_List.thy` (diff)
The file was modified	`thys/Coinductive/Quotient_TLList.thy` (diff)
The file was modified	`thys/Coinductive/ROOT` (diff)
The file was modified	`thys/Coinductive_Languages/Coinductive_Regular_Set.thy` (diff)
The file was modified	`thys/Coinductive_Languages/Context_Free_Grammar.thy` (diff)
The file was modified	`thys/Coinductive_Languages/ROOT` (diff)
The file was modified	`thys/Collections/Examples/Autoref/Buchi_Graph_Basic.thy` (diff)
The file was modified	`thys/Collections/Examples/Autoref/Coll_Test.thy` (diff)
The file was modified	`thys/Collections/Examples/Autoref/Collection_Autoref_Examples.thy` (diff)
The file was modified	`thys/Collections/Examples/Autoref/ICF_Only_Test.thy` (diff)
The file was modified	`thys/Collections/Examples/Autoref/ICF_Test.thy` (diff)
The file was modified	`thys/Collections/Examples/Autoref/Nested_DFS.thy` (diff)
The file was modified	`thys/Collections/Examples/Autoref/Simple_DFS.thy` (diff)
The file was modified	`thys/Collections/Examples/Autoref/Succ_Graph.thy` (diff)
The file was modified	`thys/Collections/Examples/ICF/Exploration.thy` (diff)
The file was modified	`thys/Collections/Examples/ICF/ICF_Examples.thy` (diff)
The file was modified	`thys/Collections/Examples/ICF/PerformanceTest.thy` (diff)
The file was modified	`thys/Collections/Examples/ICF/itp_2010.thy` (diff)
The file was modified	`thys/Collections/Examples/Refine_Monadic/Bfs_Impl.thy` (diff)
The file was modified	`thys/Collections/Examples/Refine_Monadic/Foreach_Refine.thy` (diff)
The file was modified	`thys/Collections/Examples/Refine_Monadic/Refine_Fold.thy` (diff)
The file was modified	`thys/Collections/GenCF/Gen/Gen_Comp.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/Impl/Impl_Array_Stack.thy` (diff)
The file was modified	`thys/Collections/GenCF/Impl/Impl_Bit_Set.thy` (diff)
The file was modified	`thys/Collections/GenCF/Impl/Impl_List_Map.thy` (diff)
The file was modified	`thys/Collections/GenCF/Impl/Impl_RBT_Map.thy` (diff)
The file was modified	`thys/Collections/GenCF/Impl/Impl_Uv_Set.thy` (diff)
The file was modified	`thys/Collections/GenCF/Intf/Intf_Comp.thy` (diff)
The file was modified	`thys/Collections/GenCF/Intf/Intf_Hash.thy` (diff)
The file was modified	`thys/Collections/GenCF/Intf/Intf_Map.thy` (diff)
The file was modified	`thys/Collections/GenCF/Intf/Intf_Set.thy` (diff)
The file was modified	`thys/Collections/ICF/DatRef.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/SetByMap.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/ArrayHashMap_Impl.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/ArraySetImpl.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/BinoPrioImpl.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/FTAnnotatedListImpl.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/HashSet.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/RBTMapImpl.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/RBTSetImpl.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/SkewPrioImpl.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/Trie_Impl.thy` (diff)
The file was modified	`thys/Collections/ICF/spec/PrioSpec.thy` (diff)
The file was modified	`thys/Collections/Iterator/Gen_Iterator.thy` (diff)
The file was modified	`thys/Collections/Iterator/Idx_Iterator.thy` (diff)
The file was modified	`thys/Collections/Iterator/It_to_It.thy` (diff)
The file was modified	`thys/Collections/Iterator/Proper_Iterator.thy` (diff)
The file was modified	`thys/Collections/Iterator/SetIterator.thy` (diff)
The file was modified	`thys/Collections/Iterator/SetIteratorGA.thy` (diff)
The file was modified	`thys/Collections/Lib/Assoc_List.thy` (diff)
The file was modified	`thys/Collections/Lib/Code_Target_ICF.thy` (diff)
The file was modified	`thys/Collections/Lib/Diff_Array.thy` (diff)
The file was modified	`thys/Collections/Lib/Dlist_add.thy` (diff)
The file was modified	`thys/Collections/Lib/HashCode.thy` (diff)
The file was modified	`thys/Collections/Lib/RBT_add.thy` (diff)
The file was modified	`thys/Collections/Lib/Sorted_List_Operations.thy` (diff)
The file was modified	`thys/Collections/ROOT` (diff)
The file was modified	`thys/Collections/Refine_Dflt.thy` (diff)
The file was modified	`thys/Collections/Refine_Dflt_ICF.thy` (diff)
The file was modified	`thys/Collections/Refine_Dflt_Only_ICF.thy` (diff)
The file was modified	`thys/Comparison_Sort_Lower_Bound/Comparison_Sort_Lower_Bound.thy` (diff)
The file was modified	`thys/Comparison_Sort_Lower_Bound/Linorder_Relations.thy` (diff)
The file was modified	`thys/Comparison_Sort_Lower_Bound/ROOT` (diff)
The file was modified	`thys/Completeness/PermutationLemmas.thy` (diff)
The file was modified	`thys/Completeness/ROOT` (diff)
The file was modified	`thys/Complx/ROOT` (diff)
The file was modified	`thys/Complx/SeqCatch_decomp.thy` (diff)
The file was modified	`thys/Complx/ex/SumArr.thy` (diff)
The file was modified	`thys/ConcurrentGC/Model.thy` (diff)
The file was modified	`thys/ConcurrentGC/Proofs_basis.thy` (diff)
The file was modified	`thys/ConcurrentGC/Tactics.thy` (diff)
The file was modified	`thys/ConcurrentGC/concrete/Concrete_heap.thy` (diff)
The file was modified	`thys/ConcurrentIMP/CIMP_unbounded_buffer_ex.thy` (diff)
The file was modified	`thys/Concurrent_Ref_Alg/ROOT` (diff)
The file was modified	`thys/Concurrent_Ref_Alg/Refinement_Lattice.thy` (diff)
The file was modified	`thys/Consensus_Refined/HO_Transition_System.thy` (diff)
The file was modified	`thys/Consensus_Refined/MRU/CT_Defs.thy` (diff)
The file was modified	`thys/Consensus_Refined/MRU/CT_Proofs.thy` (diff)
The file was modified	`thys/Consensus_Refined/MRU/New_Algorithm_Defs.thy` (diff)
The file was modified	`thys/Consensus_Refined/MRU/New_Algorithm_Proofs.thy` (diff)
The file was modified	`thys/Consensus_Refined/MRU/Paxos_Defs.thy` (diff)
The file was modified	`thys/Consensus_Refined/MRU/Paxos_Proofs.thy` (diff)
The file was modified	`thys/Consensus_Refined/MRU/Three_Step_MRU.thy` (diff)
The file was modified	`thys/Consensus_Refined/Observing/BenOr_Defs.thy` (diff)
The file was modified	`thys/Consensus_Refined/Observing/BenOr_Proofs.thy` (diff)
The file was modified	`thys/Consensus_Refined/Observing/Uv_Defs.thy` (diff)
The file was modified	`thys/Consensus_Refined/Observing/Uv_Proofs.thy` (diff)
The file was modified	`thys/Consensus_Refined/ROOT` (diff)
The file was modified	`thys/Consensus_Refined/Same_Vote.thy` (diff)
The file was modified	`thys/Consensus_Refined/Voting.thy` (diff)
The file was modified	`thys/Consensus_Refined/Voting/Ate_Defs.thy` (diff)
The file was modified	`thys/Consensus_Refined/Voting/Ate_Proofs.thy` (diff)
The file was modified	`thys/Consensus_Refined/Voting/OneThirdRule_Defs.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/Card_Datatype.thy` (diff)
The file was modified	`thys/Containers/Closure_Set.thy` (diff)
The file was modified	`thys/Containers/Collection_Eq.thy` (diff)
The file was modified	`thys/Containers/Collection_Order.thy` (diff)
The file was modified	`thys/Containers/Compatibility_Containers_Regular_Sets.thy` (diff)
The file was modified	`thys/Containers/Containers_Auxiliary.thy` (diff)
The file was modified	`thys/Containers/Containers_Generator.thy` (diff)
The file was modified	`thys/Containers/DList_Set.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_LC.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/ITP-2013/Benchmark_Set_Default.thy` (diff)
The file was modified	`thys/Containers/ITP-2013/Benchmark_Set_LC.thy` (diff)
The file was modified	`thys/Containers/ITP-2013/Clauses.thy` (diff)
The file was modified	`thys/Containers/Lexicographic_Order.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_ext.thy` (diff)
The file was modified	`thys/Containers/ROOT` (diff)
The file was modified	`thys/Containers/Set_Linorder.thy` (diff)
The file was modified	`thys/CoreC++/Auxiliary.thy` (diff)
The file was modified	`thys/CoreC++/Execute.thy` (diff)
The file was modified	`thys/CryptHOL/CryptHOL.thy` (diff)
The file was modified	`thys/CryptHOL/Cyclic_Group.thy` (diff)
The file was modified	`thys/CryptHOL/Cyclic_Group_SPMF.thy` (diff)
The file was modified	`thys/CryptHOL/Environment_Functor.thy` (diff)
The file was modified	`thys/CryptHOL/Generative_Probabilistic_Value.thy` (diff)
The file was modified	`thys/CryptHOL/Misc_CryptHOL.thy` (diff)
The file was modified	`thys/CryptHOL/Negligible.thy` (diff)
The file was modified	`thys/CryptHOL/ROOT` (diff)
The file was modified	`thys/CryptHOL/SPMF_Applicative.thy` (diff)
The file was modified	`thys/CryptHOL/Set_Applicative.thy` (diff)
The file was modified	`thys/DFS_Framework/Examples/Cyc_Check.thy` (diff)
The file was modified	`thys/DFS_Framework/Examples/DFS_Find_Path.thy` (diff)
The file was modified	`thys/DFS_Framework/Examples/Feedback_Arcs.thy` (diff)
The file was modified	`thys/DFS_Framework/Examples/Reachable_Nodes.thy` (diff)
The file was modified	`thys/DFS_Framework/Impl/Structural/Rec_Impl.thy` (diff)
The file was modified	`thys/DFS_Framework/Impl/Structural/Tailrec_Impl.thy` (diff)
The file was modified	`thys/DFS_Framework/Invars/DFS_Invars_SCC.thy` (diff)
The file was modified	`thys/DFS_Framework/Misc/DFS_Framework_Misc.thy` (diff)
The file was modified	`thys/DFS_Framework/Misc/DFS_Framework_Refine_Aux.thy` (diff)
The file was modified	`thys/DFS_Framework/Misc/Impl_Rev_Array_Stack.thy` (diff)
The file was modified	`thys/DFS_Framework/Misc/On_Stack.thy` (diff)
The file was modified	`thys/DFS_Framework/Param_DFS.thy` (diff)
The file was modified	`thys/DFS_Framework/ROOT` (diff)
The file was modified	`thys/DPT-SAT-Solver/DPT_SAT_Solver.thy` (diff)
The file was modified	`thys/DataRefinementIBP/Preliminaries.thy` (diff)
The file was modified	`thys/DataRefinementIBP/ROOT` (diff)
The file was modified	`thys/Datatype_Order_Generator/Derive.thy` (diff)
The file was modified	`thys/Datatype_Order_Generator/Derive_Aux.thy` (diff)
The file was modified	`thys/Datatype_Order_Generator/Derive_Examples.thy` (diff)
The file was modified	`thys/Datatype_Order_Generator/Hash_Generator.thy` (diff)
The file was modified	`thys/Datatype_Order_Generator/ROOT` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/MutableRef.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/ROOT` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/SystemF.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/ValuesFSet.thy` (diff)
The file was modified	`thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II.thy` (diff)
The file was modified	`thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II_Aux.thy` (diff)
The file was modified	`thys/Decreasing-Diagrams-II/ROOT` (diff)
The file was modified	`thys/Decreasing-Diagrams/Decreasing_Diagrams.thy` (diff)
The file was modified	`thys/Decreasing-Diagrams/ROOT` (diff)
The file was modified	`thys/Deep_Learning/DL_Concrete_Matrices.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Deep_Model.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Deep_Model_Poly.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Flatten_Matrix.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Fundamental_Theorem_Network_Capacity.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Missing_Matrix.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Missing_VS_Connect.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Missing_Vector_Space.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Network.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Rank.thy` (diff)
The file was modified	`thys/Deep_Learning/DL_Submatrix.thy` (diff)
The file was modified	`thys/Deep_Learning/Lebesgue_Functional.thy` (diff)
The file was modified	`thys/Deep_Learning/PP_Poly_Mapping.thy` (diff)
The file was modified	`thys/Deep_Learning/PP_Univariate.thy` (diff)
The file was modified	`thys/Deep_Learning/ROOT` (diff)
The file was modified	`thys/Deep_Learning/Tensor_Matricization.thy` (diff)
The file was modified	`thys/Deep_Learning/Tensor_Plus.thy` (diff)
The file was modified	`thys/Density_Compiler/Density_Predicates.thy` (diff)
The file was modified	`thys/Density_Compiler/ROOT` (diff)
The file was modified	`thys/Dependent_SIFUM_Refinement/CompositionalRefinement.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Refinement/Examples/Eg1.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Refinement/Examples/Eg1RefinementTrivial.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Refinement/Examples/Eg2.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Refinement/Examples/EgHighBranchRevC.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Type_Systems/Examples/Example_Swap_Add.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Type_Systems/Examples/Example_TypeSystem.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Type_Systems/Examples/TypeSystemTactics.thy` (diff)
The file was modified	`thys/Derangements/Derangements.thy` (diff)
The file was modified	`thys/Derangements/ROOT` (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_Real.thy` (diff)
The file was modified	`thys/Deriving/Comparator_Generator/RBT_Comparator_Impl.thy` (diff)
The file was modified	`thys/Deriving/Comparator_Generator/RBT_Compare_Order_Impl.thy` (diff)
The file was modified	`thys/Deriving/Countable_Generator/Countable_Generator.thy` (diff)
The file was modified	`thys/Deriving/Derive_Examples.thy` (diff)
The file was modified	`thys/Deriving/Hash_Generator/Hash_Generator.thy` (diff)
The file was modified	`thys/Deriving/ROOT` (diff)
The file was modified	`thys/Descartes_Sign_Rule/Descartes_Sign_Rule.thy` (diff)
The file was modified	`thys/Dict_Construction/Dict_Construction.thy` (diff)
The file was modified	`thys/Dict_Construction/ROOT` (diff)
The file was modified	`thys/Dict_Construction/Test_Dict_Construction.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Axioms.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Bound_Effect.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Coincidence.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Denotational_Semantics.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Differential_Axioms.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Differential_Dynamic_Logic.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Frechet_Correctness.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Lib.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Pretty_Printer.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Proof_Checker.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Static_Semantics.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/USubst.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/USubst_Lemma.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Uniform_Renaming.thy` (diff)
The file was modified	`thys/Dijkstra_Shortest_Path/Dijkstra.thy` (diff)
The file was modified	`thys/Dijkstra_Shortest_Path/Dijkstra_Impl.thy` (diff)
The file was modified	`thys/Dijkstra_Shortest_Path/Dijkstra_Impl_Adet.thy` (diff)
The file was modified	`thys/Dijkstra_Shortest_Path/GraphSpec.thy` (diff)
The file was modified	`thys/Dijkstra_Shortest_Path/ROOT` (diff)
The file was modified	`thys/Discrete_Summation/Factorials.thy` (diff)
The file was modified	`thys/DynamicArchitectures/Configuration_Traces.thy` (diff)
The file was modified	`thys/DynamicArchitectures/ROOT` (diff)
The file was modified	`thys/Dynamic_Tables/Tables_real.thy` (diff)
The file was modified	`thys/E_Transcendental/E_Transcendental.thy` (diff)
The file was modified	`thys/E_Transcendental/ROOT` (diff)
The file was modified	`thys/Echelon_Form/Cayley_Hamilton_Compatible.thy` (diff)
The file was modified	`thys/Echelon_Form/Code_Cayley_Hamilton.thy` (diff)
The file was modified	`thys/Echelon_Form/Code_Cayley_Hamilton_IArrays.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_IArrays.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_Inverse.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_Inverse_IArrays.thy` (diff)
The file was modified	`thys/Echelon_Form/Examples_Echelon_Form_Abstract.thy` (diff)
The file was modified	`thys/Echelon_Form/Examples_Echelon_Form_IArrays.thy` (diff)
The file was modified	`thys/Echelon_Form/ROOT` (diff)
The file was modified	`thys/Echelon_Form/Rings2.thy` (diff)
The file was modified	`thys/Efficient-Mergesort/Efficient_Sort.thy` (diff)
The file was modified	`thys/Elliptic_Curves_Group_Law/Elliptic_Axclass.thy` (diff)
The file was modified	`thys/Elliptic_Curves_Group_Law/Elliptic_Locale.thy` (diff)
The file was modified	`thys/Elliptic_Curves_Group_Law/Elliptic_Test.thy` (diff)
The file was modified	`thys/Elliptic_Curves_Group_Law/ROOT` (diff)
The file was modified	`thys/Encodability_Process_Calculi/Relations.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Fekete.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Invariants.thy` (diff)
The file was modified	`thys/Ergodic_Theory/SG_Library_Complement.thy` (diff)
The file was modified	`thys/Euler_MacLaurin/Euler_MacLaurin.thy` (diff)
The file was modified	`thys/Euler_MacLaurin/Euler_MacLaurin_Landau.thy` (diff)
The file was modified	`thys/Euler_MacLaurin/ROOT` (diff)
The file was modified	`thys/Euler_Partition/Euler_Partition.thy` (diff)
The file was modified	`thys/FOL-Fitting/FOL_Fitting.thy` (diff)
The file was modified	`thys/FOL_Harrison/FOL_Harrison.thy` (diff)
The file was modified	`thys/FOL_Harrison/ROOT` (diff)
The file was modified	`thys/Featherweight_OCL/ROOT` (diff)
The file was modified	`thys/Featherweight_OCL/UML_Types.thy` (diff)
The file was modified	`thys/Fermat3_4/Fermat4.thy` (diff)
The file was modified	`thys/Fermat3_4/Quad_Form.thy` (diff)
The file was modified	`thys/FinFun/FinFun.thy` (diff)
The file was modified	`thys/Finger-Trees/Test.thy` (diff)
The file was modified	`thys/Finite_Automata_HF/Finite_Automata_HF.thy` (diff)
The file was modified	`thys/Finite_Automata_HF/ROOT` (diff)
The file was modified	`thys/Fisher_Yates/Fisher_Yates.thy` (diff)
The file was modified	`thys/Floyd_Warshall/Recursion_Combinators.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/Arch.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/ArchComp.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/ArchCompAux.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/IArray_Syntax.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/ROOT` (diff)
The file was modified	`thys/Flyspeck-Tame/Worklist.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/Disjoin_Transform.thy` (diff)
The file was modified	`thys/Formal_SSA/FormalSSA_Misc.thy` (diff)
The file was modified	`thys/Formal_SSA/Generic_Interpretation.thy` (diff)
The file was modified	`thys/Formal_SSA/Graph_path.thy` (diff)
The file was modified	`thys/Formal_SSA/Mapping_Exts.thy` (diff)
The file was modified	`thys/Formal_SSA/RBT_Mapping_Exts.thy` (diff)
The file was modified	`thys/Formal_SSA/ROOT` (diff)
The file was modified	`thys/Formal_SSA/SSA_CFG.thy` (diff)
The file was modified	`thys/Formal_SSA/SSA_CFG_code.thy` (diff)
The file was modified	`thys/Formal_SSA/WhileGraphSSA.thy` (diff)
The file was modified	`thys/Formal_SSA/While_Combinator_Exts.thy` (diff)
The file was modified	`thys/Formula_Derivatives/Abstract_Formula.thy` (diff)
The file was modified	`thys/Formula_Derivatives/Automaton.thy` (diff)
The file was modified	`thys/Formula_Derivatives/FSet_More.thy` (diff)
The file was modified	`thys/Formula_Derivatives/Presburger_Examples.thy` (diff)
The file was modified	`thys/Formula_Derivatives/Presburger_Formula.thy` (diff)
The file was modified	`thys/Formula_Derivatives/ROOT` (diff)
The file was modified	`thys/Formula_Derivatives/WS1S_Alt_Examples.thy` (diff)
The file was modified	`thys/Formula_Derivatives/WS1S_Examples.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_Examples.thy` (diff)
The file was modified	`thys/Formula_Derivatives/While_Default.thy` (diff)
The file was modified	`thys/Free-Groups/C2.thy` (diff)
The file was modified	`thys/Free-Groups/Cancelation.thy` (diff)
The file was modified	`thys/Free-Groups/FreeGroups.thy` (diff)
The file was modified	`thys/Free-Groups/Generators.thy` (diff)
The file was modified	`thys/Free-Groups/Isomorphisms.thy` (diff)
The file was modified	`thys/Free-Groups/PingPongLemma.thy` (diff)
The file was modified	`thys/Free-Groups/ROOT` (diff)
The file was modified	`thys/Free-Groups/UnitGroup.thy` (diff)
The file was modified	`thys/Functional-Automata/MaxPrefix.thy` (diff)
The file was modified	`thys/Functional-Automata/ROOT` (diff)
The file was modified	`thys/Functional-Automata/RegExp2NA.thy` (diff)
The file was modified	`thys/Functional-Automata/RegExp2NAe.thy` (diff)
The file was modified	`thys/Functional-Automata/RegSet_of_nat_DA.thy` (diff)
The file was modified	`thys/Gabow_SCC/Find_Path.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_GBG_Code.thy` (diff)
The file was modified	`thys/Gabow_SCC/Gabow_SCC_Code.thy` (diff)
The file was modified	`thys/Gabow_SCC/Gabow_Skeleton.thy` (diff)
The file was modified	`thys/Gabow_SCC/Gabow_Skeleton_Code.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/Diffie_Hellman.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/Elgamal.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/Guessing_Many_One.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/Hashed_Elgamal.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/IND_CCA2.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/IND_CCA2_sym.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/IND_CPA.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/IND_CPA_PK.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/IND_CPA_PK_Single.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/PRF_IND_CPA.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/PRF_UHF.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/PRF_UPF_IND_CCA.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/Pseudo_Random_Function.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/Pseudo_Random_Permutation.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/RP_RF.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/SUF_CMA.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/Unpredictable_Function.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Code_Bit.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Code_Generation_IArrays_SML.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Code_Matrix.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Code_Rational.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Code_Real_Approx_By_Float_Haskell.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Code_Set.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Elementary_Operations.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Examples_Gauss_Jordan_Abstract.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Examples_Gauss_Jordan_IArrays.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Gauss_Jordan_PA.thy` (diff)
The file was modified	`thys/Gauss_Jordan/IArray_Addenda.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Matrix_To_IArray.thy` (diff)
The file was modified	`thys/Gauss_Jordan/ROOT` (diff)
The file was modified	`thys/Gauss_Jordan/Rank.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Rref.thy` (diff)
The file was modified	`thys/Girth_Chromatic/Girth_Chromatic.thy` (diff)
The file was modified	`thys/Girth_Chromatic/Girth_Chromatic_Misc.thy` (diff)
The file was modified	`thys/GraphMarkingIBP/ROOT` (diff)
The file was modified	`thys/GraphMarkingIBP/SetMark.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/Funpow.thy` (diff)
The file was modified	`thys/Graph_Theory/Kuratowski.thy` (diff)
The file was modified	`thys/Graph_Theory/ROOT` (diff)
The file was modified	`thys/Graph_Theory/Shortest_Path.thy` (diff)
The file was modified	`thys/Graph_Theory/Stuff.thy` (diff)
The file was modified	`thys/Groebner_Bases/Computations.thy` (diff)
The file was modified	`thys/Groebner_Bases/Confluence.thy` (diff)
The file was modified	`thys/Groebner_Bases/Groebner_Bases.thy` (diff)
The file was modified	`thys/Groebner_Bases/ROOT` (diff)
The file was modified	`thys/Group-Ring-Module/Algebra1.thy` (diff)
The file was modified	`thys/Group-Ring-Module/Algebra4.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/Definedness.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/HOLCF_Main.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/ROOT` (diff)
The file was modified	`thys/HOLCF-Prelude/examples/Sieve_Primes.thy` (diff)
The file was modified	`thys/HRB-Slicing/JinjaVM_Inter/JVMCFG.thy` (diff)
The file was modified	`thys/Heard_Of/ROOT` (diff)
The file was modified	`thys/Heard_Of/Reduction.thy` (diff)
The file was modified	`thys/HereditarilyFinite/HF.thy` (diff)
The file was modified	`thys/HereditarilyFinite/ROOT` (diff)
The file was modified	`thys/Hermite/Hermite.thy` (diff)
The file was modified	`thys/Hermite/Hermite_IArrays.thy` (diff)
The file was modified	`thys/Hermite/ROOT` (diff)
The file was modified	`thys/HotelKeyCards/Notation.thy` (diff)
The file was modified	`thys/HyperCTL/Deep.thy` (diff)
The file was modified	`thys/HyperCTL/Prelim.thy` (diff)
The file was modified	`thys/HyperCTL/ROOT` (diff)
The file was modified	`thys/IP_Addresses/IP_Address_Parser.thy` (diff)
The file was modified	`thys/IP_Addresses/IP_Address_toString.thy` (diff)
The file was modified	`thys/IP_Addresses/Lib_Word_toString.thy` (diff)
The file was modified	`thys/IP_Addresses/NumberWang_IPv4.thy` (diff)
The file was modified	`thys/IP_Addresses/NumberWang_IPv6.thy` (diff)
The file was modified	`thys/IP_Addresses/ROOT` (diff)
The file was modified	`thys/IP_Addresses/WordInterval.thy` (diff)
The file was modified	`thys/IP_Addresses/WordInterval_Sorted.thy` (diff)
The file was modified	`thys/IP_Addresses/Word_More.thy` (diff)
The file was modified	`thys/IP_Addresses/Word_Next.thy` (diff)
The file was modified	`thys/Imperative_Insertion_Sort/Imperative_Insertion_Sort.thy` (diff)
The file was modified	`thys/Imperative_Insertion_Sort/Imperative_Loops.thy` (diff)
The file was modified	`thys/Imperative_Insertion_Sort/ROOT` (diff)
The file was modified	`thys/Incompleteness/ROOT` (diff)
The file was modified	`thys/Incompleteness/SyntaxN.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Abstract_Formula.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Abstract_Rules_To_Incredible.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Entailment.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Incredible_Deduction.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Incredible_Predicate_Tasks.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Incredible_Signatures.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Incredible_Trees.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Indexed_FSet.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Natural_Deduction.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Predicate_Formulas.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Propositional_Formulas.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/ROOT` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Rose_Tree.thy` (diff)
The file was modified	`thys/InfPathElimination/Conf.thy` (diff)
The file was modified	`thys/InfPathElimination/SymExec.thy` (diff)
The file was modified	`thys/InformationFlowSlicing/LiftingIntra.thy` (diff)
The file was modified	`thys/InformationFlowSlicing/NonInterferenceIntra.thy` (diff)
The file was modified	`thys/InformationFlowSlicing/NonInterferenceWhile.thy` (diff)
The file was modified	`thys/InformationFlowSlicing_Inter/NonInterferenceInter.thy` (diff)
The file was modified	`thys/Integration/RealRandVar.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Access_Matrix_Embeddings.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Common/WordInterval_Lists.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Common/Word_Upto.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Code_haskell.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Contrived/Contrived_Example.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Fail/Ports_Fail.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/IPPartEval/IP_Address_Space_Examples_All_Small.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Parser_Test/Parser_Test.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Ringofsaturn_com/Analyze_Ringofsaturn_com.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/SQRL_Shorewall/Analyze_SQRL_Shorewall.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/SQRL_Shorewall/SQRL_2015_nospoof.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Small_Examples.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Synology_Diskstation_DS414/Analyze_Synology_Diskstation.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Synology_Diskstation_DS414/iptables_Ln_tuned_parsed.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/TUM_Net_Firewall/Analyze_TUM_Net_Firewall.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/containern/Analyze_Containern.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/medium-sized-company/Analyze_medium_sized_company.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/sns.ias.edu/SNS_IAS_Eduroam_Spoofing.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/topoS_generated/Analyze_topos_generated.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Firewall_Common.thy` (diff)
The file was modified	`thys/Iptables_Semantics/No_Spoof_Embeddings.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Common_Primitive_Syntax.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Common_Primitive_toString.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Conntrack_State.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Conntrack_State_Transform.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/IpAddresses.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/L4_Protocol_Flags.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Parser6.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Ports.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Routing_IpAssmt.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Tagged_Packet.thy` (diff)
The file was modified	`thys/Iptables_Semantics/ROOT` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Goto.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Simple_Firewall/SimpleFw_Compliance.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/Init.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/Init_rbt.thy` (diff)
The file was modified	`thys/Jinja/BV/BVExample.thy` (diff)
The file was modified	`thys/Jinja/Common/TypeRel.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/DFA/Semilat.thy` (diff)
The file was modified	`thys/Jinja/J/execute_Bigstep.thy` (diff)
The file was modified	`thys/Jinja/JVM/JVMListExample.thy` (diff)
The file was modified	`thys/Jinja/ROOT` (diff)
The file was modified	`thys/JinjaThreads/Basic/Auxiliary.thy` (diff)
The file was modified	`thys/JinjaThreads/Basic/Basic_Main.thy` (diff)
The file was modified	`thys/JinjaThreads/Basic/JT_ICF.thy` (diff)
The file was modified	`thys/JinjaThreads/Basic/Set_Monad.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/Value.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J0.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/J1Heap.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/J1WellForm.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/JJ1WellForm.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/TypeComp.thy` (diff)
The file was modified	`thys/JinjaThreads/DFA/Semilat.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/Code_Generation.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/TypeRelRefine.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/LTS.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_Heap.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Interp.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Spec.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_Completion.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/CompositionSeries.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/GroupIsoClasses.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/JordanHolder.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/MaximalNormalSubgroups.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/ROOT` (diff)
The file was modified	`thys/Jordan_Hoelder/SimpleGroups.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/SndIsomorphismGrp.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/SubgroupsAndNormalSubgroups.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Char_Poly.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Complexity_Carrier.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Conjugate.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Derivation_Bound.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Determinant.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Determinant_Impl.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gauss_Jordan_IArray_Impl.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Comparison.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/Missing_Permutations.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Missing_Ring.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Missing_VectorSpace.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/ROOT` (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_Arctic.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Show_Matrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/VS_Connect.thy` (diff)
The file was modified	`thys/KAD/Domain_Semiring.thy` (diff)
The file was modified	`thys/KAD/Modal_Kleene_Algebra_Models.thy` (diff)
The file was modified	`thys/KAD/ROOT` (diff)
The file was modified	`thys/KAT_and_DRA/SingleSorted/Conway_Tests.thy` (diff)
The file was modified	`thys/KAT_and_DRA/SingleSorted/DRAT.thy` (diff)
The file was modified	`thys/KAT_and_DRA/SingleSorted/KAT.thy` (diff)
The file was modified	`thys/KAT_and_DRA/SingleSorted/KAT_Models.thy` (diff)
The file was modified	`thys/KAT_and_DRA/SingleSorted/PHL_DRAT.thy` (diff)
The file was modified	`thys/KAT_and_DRA/SingleSorted/PHL_KAT.thy` (diff)
The file was modified	`thys/KAT_and_DRA/SingleSorted/Test_Dioid.thy` (diff)
The file was modified	`thys/KAT_and_DRA/TwoSorted/DRAT2.thy` (diff)
The file was modified	`thys/KAT_and_DRA/TwoSorted/KAT2.thy` (diff)
The file was modified	`thys/KBPs/ClockView.thy` (diff)
The file was modified	`thys/KBPs/Examples.thy` (diff)
The file was modified	`thys/KBPs/Extra.thy` (diff)
The file was modified	`thys/KBPs/List_local.thy` (diff)
The file was modified	`thys/KBPs/ODList.thy` (diff)
The file was modified	`thys/KBPs/Robot.thy` (diff)
The file was modified	`thys/KBPs/SPRViewDet.thy` (diff)
The file was modified	`thys/KBPs/SPRViewSingle.thy` (diff)
The file was modified	`thys/KBPs/Trie2.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Dioid_Models.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Matrix.thy` (diff)
The file was modified	`thys/Knot_Theory/Kauffman_Matrix.thy` (diff)
The file was modified	`thys/Knot_Theory/ROOT` (diff)
The file was modified	`thys/Koenigsberg_Friendship/FriendshipTheory.thy` (diff)
The file was modified	`thys/Koenigsberg_Friendship/KoenigsbergBridge.thy` (diff)
The file was modified	`thys/Koenigsberg_Friendship/MoreGraph.thy` (diff)
The file was modified	`thys/Koenigsberg_Friendship/ROOT` (diff)
The file was modified	`thys/LOFT/Examples/OF_conv_test/OF_conv_test.thy` (diff)
The file was modified	`thys/LOFT/Examples/RFC2544/RFC2544.thy` (diff)
The file was modified	`thys/LOFT/LinuxRouter_OpenFlow_Translation.thy` (diff)
The file was modified	`thys/LOFT/OpenFlow_Documentation.thy` (diff)
The file was modified	`thys/LOFT/OpenFlow_Matches.thy` (diff)
The file was modified	`thys/LOFT/OpenFlow_Serialize.thy` (diff)
The file was modified	`thys/LOFT/Semantics_OpenFlow.thy` (diff)
The file was modified	`thys/LTL/LTL.thy` (diff)
The file was modified	`thys/LTL/LTL_Rewrite.thy` (diff)
The file was modified	`thys/LTL/example/LTL_Example.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Auxiliary/List2.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Auxiliary/Mapping2.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Auxiliary/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_Compat.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Impl/LTL_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_FGXU.thy` (diff)
The file was modified	`thys/LTL_to_DRA/ROOT` (diff)
The file was modified	`thys/LTL_to_GBA/LTL_Stutter.thy` (diff)
The file was modified	`thys/LTL_to_GBA/LTL_to_GBA.thy` (diff)
The file was modified	`thys/LTL_to_GBA/LTL_to_GBA_impl.thy` (diff)
The file was modified	`thys/LTL_to_GBA/ROOT` (diff)
The file was modified	`thys/Lam-ml-Normalization/Lam_ml.thy` (diff)
The file was modified	`thys/Lam-ml-Normalization/ROOT` (diff)
The file was modified	`thys/Lambda_Free_KBOs/Lambda_Free_KBO_Util.thy` (diff)
The file was modified	`thys/Lambda_Free_KBOs/Lambda_Free_TKBO_Coefs.thy` (diff)
The file was modified	`thys/Lambda_Free_KBOs/ROOT` (diff)
The file was modified	`thys/Lambda_Free_RPOs/Extension_Orders.thy` (diff)
The file was modified	`thys/Lambda_Free_RPOs/Lambda_Free_Util.thy` (diff)
The file was modified	`thys/Lambda_Free_RPOs/ROOT` (diff)
The file was modified	`thys/Landau_Symbols/Group_Sort.thy` (diff)
The file was modified	`thys/Landau_Symbols/Landau_Real_Products.thy` (diff)
The file was modified	`thys/Landau_Symbols/Landau_Symbols_Definition.thy` (diff)
The file was modified	`thys/Latin_Square/Latin_Square.thy` (diff)
The file was modified	`thys/Launchbury/AList-Utils.thy` (diff)
The file was modified	`thys/Launchbury/Abstract-Denotational-Props.thy` (diff)
The file was modified	`thys/Launchbury/AbstractDenotational.thy` (diff)
The file was modified	`thys/Launchbury/Adequacy.thy` (diff)
The file was modified	`thys/Launchbury/C.thy` (diff)
The file was modified	`thys/Launchbury/CorrectnessOriginal.thy` (diff)
The file was modified	`thys/Launchbury/CorrectnessResourced.thy` (diff)
The file was modified	`thys/Launchbury/Denotational-Related.thy` (diff)
The file was modified	`thys/Launchbury/EvalHeap.thy` (diff)
The file was modified	`thys/Launchbury/EverythingAdequacy.thy` (diff)
The file was modified	`thys/Launchbury/HOLCF-Join.thy` (diff)
The file was modified	`thys/Launchbury/HOLCF-Meet.thy` (diff)
The file was modified	`thys/Launchbury/HOLCF-Utils.thy` (diff)
The file was modified	`thys/Launchbury/HeapSemantics.thy` (diff)
The file was modified	`thys/Launchbury/Mono-Nat-Fun.thy` (diff)
The file was modified	`thys/Launchbury/Nominal-Utils.thy` (diff)
The file was modified	`thys/Launchbury/ROOT` (diff)
The file was modified	`thys/Launchbury/ResourcedAdequacy.thy` (diff)
The file was modified	`thys/Launchbury/Value.thy` (diff)
The file was modified	`thys/Launchbury/Vars.thy` (diff)
The file was modified	`thys/Lazy-Lists-II/LList2.thy` (diff)
The file was modified	`thys/Lehmer/Lehmer.thy` (diff)
The file was modified	`thys/Lehmer/ROOT` (diff)
The file was modified	`thys/LightweightJava/Lightweight_Java_Definition.thy` (diff)
The file was modified	`thys/LightweightJava/Lightweight_Java_Proof.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/LinArith.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/Logic.thy` (diff)
The file was modified	`thys/LinearQuantifierElim/Thys/PresArith.thy` (diff)
The file was modified	`thys/Liouville_Numbers/Liouville_Numbers.thy` (diff)
The file was modified	`thys/Liouville_Numbers/Liouville_Numbers_Misc.thy` (diff)
The file was modified	`thys/Liouville_Numbers/ROOT` (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/ListInf/ListInf_Prefix.thy` (diff)
The file was modified	`thys/List_Update/Inversion.thy` (diff)
The file was modified	`thys/List_Update/RExp_Var.thy` (diff)
The file was modified	`thys/List_Update/ROOT` (diff)
The file was modified	`thys/Locally-Nameless-Sigma/ROOT` (diff)
The file was modified	`thys/Locally-Nameless-Sigma/Sigma/ParRed.thy` (diff)
The file was modified	`thys/Lower_Semicontinuous/Lower_Semicontinuous.thy` (diff)
The file was modified	`thys/Lp/Functional_Spaces.thy` (diff)
The file was modified	`thys/MFMC_Countable/MFMC_Misc.thy` (diff)
The file was modified	`thys/MFMC_Countable/ROOT` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Init_Normalization.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/List_More.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/M2L_Examples.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Pi_Equivalence_Checking.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Pi_Regular_Exp.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Pi_Regular_Exp_Dual.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Pi_Regular_Operators.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/ROOT` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/WS1S.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/WS1S_Examples.thy` (diff)
The file was modified	`thys/Markov_Models/Markov_Models_Auxiliary.thy` (diff)
The file was modified	`thys/Markov_Models/ROOT` (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/Matrix/Ordered_Semiring.thy` (diff)
The file was modified	`thys/Matrix/ROOT` (diff)
The file was modified	`thys/Matrix_Tensor/Matrix_Tensor.thy` (diff)
The file was modified	`thys/Matrix_Tensor/ROOT` (diff)
The file was modified	`thys/Minimal_SSA/Irreducible.thy` (diff)
The file was modified	`thys/Minkowskis_Theorem/Minkowskis_Theorem.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/FS_Set.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/Nominal_Bounded_Set.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/Nominal_Wellfounded.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/ROOT` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/Residual.thy` (diff)
The file was modified	`thys/MonoBoolTranAlgebra/Mono_Bool_Tran.thy` (diff)
The file was modified	`thys/MonoidalCategory/FreeMonoidalCategory.thy` (diff)
The file was modified	`thys/MonoidalCategory/MonoidalCategory.thy` (diff)
The file was modified	`thys/Monomorphic_Monad/Monomorphic_Monad.thy` (diff)
The file was modified	`thys/MuchAdoAboutTwo/MuchAdoAboutTwo.thy` (diff)
The file was modified	`thys/Multirelations/C_Algebras.thy` (diff)
The file was modified	`thys/Multirelations/ROOT` (diff)
The file was modified	`thys/Myhill-Nerode/Closures.thy` (diff)
The file was modified	`thys/Myhill-Nerode/Closures2.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/Myhill-Nerode/Myhill_1.thy` (diff)
The file was modified	`thys/Myhill-Nerode/Myhill_2.thy` (diff)
The file was modified	`thys/Myhill-Nerode/ROOT` (diff)
The file was modified	`thys/Nat-Interval-Logic/IL_Interval.thy` (diff)
The file was modified	`thys/Native_Word/Code_Target_Bits_Int.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/Native_Word_Test.thy` (diff)
The file was modified	`thys/Native_Word/ROOT` (diff)
The file was modified	`thys/Native_Word/Uint.thy` (diff)
The file was modified	`thys/Native_Word/Word_Misc.thy` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/McCarthy_91.thy` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/Multiset_More.thy` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/Nested_Multiset.thy` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/ROOT` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/Syntactic_Ordinal.thy` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/Syntactic_Ordinal_Bridge.thy` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/Unary_PCF.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Lib/Efficient_Distinct.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Lib/FiniteListGraph.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Lib/FiniteListGraph_Impl.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/ROOT` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_DomainHierarchyNG.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Library.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Vertices.thy` (diff)
The file was modified	`thys/Nominal2/Nominal2_Abs.thy` (diff)
The file was modified	`thys/Nominal2/Nominal2_Base.thy` (diff)
The file was modified	`thys/Nominal2/Nominal2_FCB.thy` (diff)
The file was modified	`thys/Nominal2/ROOT` (diff)
The file was modified	`thys/Noninterference_Concurrent_Composition/ConcurrentComposition.thy` (diff)
The file was modified	`thys/Noninterference_Generic_Unwinding/GenericUnwinding.thy` (diff)
The file was modified	`thys/Noninterference_Generic_Unwinding/ROOT` (diff)
The file was modified	`thys/Noninterference_Inductive_Unwinding/InductiveUnwinding.thy` (diff)
The file was modified	`thys/Noninterference_Inductive_Unwinding/ROOT` (diff)
The file was modified	`thys/Noninterference_Ipurge_Unwinding/IpurgeUnwinding.thy` (diff)
The file was modified	`thys/Noninterference_Ipurge_Unwinding/ROOT` (diff)
The file was modified	`thys/Noninterference_Sequential_Composition/Propaedeutics.thy` (diff)
The file was modified	`thys/Noninterference_Sequential_Composition/ROOT` (diff)
The file was modified	`thys/Optics/Lens_State.thy` (diff)
The file was modified	`thys/Optics/ROOT` (diff)
The file was modified	`thys/Optics/Two.thy` (diff)
The file was modified	`thys/Ordinals_and_Cardinals/Cardinal_Order_Relation_discontinued.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Example3.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Example_Utilities.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Example_Variational_Equation.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Lorenz/Initials.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Flow.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Library/Bounded_Linear_Operator.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Library/MVT_Ex.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Library/Multivariate_Taylor.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/One_Step_Method.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Optimize_Float.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Optimize_Integer.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Plot.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Print.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Refine_Rigorous_Numerics_Aform.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/ODE_Numerics.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/ROOT` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Refinement/Autoref_Misc.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Refinement/GenCF_No_Comp.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Refinement/Refine_Dflt_No_Comp.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Refinement/Weak_Set.thy` (diff)
The file was modified	`thys/PCF/Basis.thy` (diff)
The file was modified	`thys/PCF/ROOT` (diff)
The file was modified	`thys/POPLmark-deBruijn/Execute.thy` (diff)
The file was modified	`thys/Pairing_Heap/Pairing_Heap_List1.thy` (diff)
The file was modified	`thys/Pairing_Heap/Pairing_Heap_List2.thy` (diff)
The file was modified	`thys/Pairing_Heap/Pairing_Heap_Tree.thy` (diff)
The file was modified	`thys/Pairing_Heap/ROOT` (diff)
The file was modified	`thys/Parity_Game/Graph_TheoryCompatibility.thy` (diff)
The file was modified	`thys/Parity_Game/MoreCoinductiveList.thy` (diff)
The file was modified	`thys/Parity_Game/ROOT` (diff)
The file was modified	`thys/Partial_Function_MR/Partial_Function_MR_Examples.thy` (diff)
The file was modified	`thys/Partial_Function_MR/ROOT` (diff)
The file was modified	`thys/Password_Authentication_Protocol/Propaedeutics.thy` (diff)
The file was modified	`thys/Password_Authentication_Protocol/ROOT` (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/Perron_Frobenius/Bij_Nat.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Cancel_Card_Constraint.thy` (diff)
The file was modified	`thys/Perron_Frobenius/HMA_Connect.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Perron_Frobenius.thy` (diff)
The file was modified	`thys/Perron_Frobenius/ROOT` (diff)
The file was modified	`thys/Perron_Frobenius/Spectral_Radius_Theory.thy` (diff)
The file was modified	`thys/Pi_Calculus/Agent.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Digraph_Map_Impl.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Executable_Permutations.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Graph_Genus.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/List_Aux.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Permutations_2.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Planar_Subgraph.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Reachablen.thy` (diff)
The file was modified	`thys/Planarity_Certificates/ROOT` (diff)
The file was modified	`thys/Planarity_Certificates/Verification/Check_Non_Planarity_Impl.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Verification/Check_Non_Planarity_Verification.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Verification/Check_Planarity_Verification.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Verification/Setup_AutoCorres.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Verification/Simpl_Anno.thy` (diff)
The file was modified	`thys/Planarity_Certificates/l4v/lib/Lib.thy` (diff)
The file was modified	`thys/Planarity_Certificates/l4v/lib/wp/WP.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Dvd_Int_Poly.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Explicit_Roots.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Fundamental_Theorem_Algebra_Factorized.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Gauss_Lemma.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Kronecker_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/Missing_Polynomial_Factorial.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Order_Polynomial.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Polynomial_Divisibility.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Precomputation.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Prime_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/ROOT` (diff)
The file was modified	`thys/Polynomial_Factorization/Rational_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Square_Free_Factorization.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Improved_Code_Equations.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Is_Rat_To_Rat.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Polynomial.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/Newton_Interpolation.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/ROOT` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom_Poly.thy` (diff)
The file was modified	`thys/Polynomials/NZM.thy` (diff)
The file was modified	`thys/Polynomials/Poly_Lists.thy` (diff)
The file was modified	`thys/Polynomials/Polynomials.thy` (diff)
The file was modified	`thys/Polynomials/ROOT` (diff)
The file was modified	`thys/Posix-Lexing/Lexer.thy` (diff)
The file was modified	`thys/Posix-Lexing/ROOT` (diff)
The file was modified	`thys/Posix-Lexing/Simplifying.thy` (diff)
The file was modified	`thys/Possibilistic_Noninterference/Interface.thy` (diff)
The file was modified	`thys/Pratt_Certificate/Pratt_Certificate.thy` (diff)
The file was modified	`thys/Presburger-Automata/Exec.thy` (diff)
The file was modified	`thys/Presburger-Automata/Presburger_Automata.thy` (diff)
The file was modified	`thys/Priority_Queue_Braun/Priority_Queue_Braun.thy` (diff)
The file was modified	`thys/Priority_Queue_Braun/ROOT` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Interface.thy` (diff)
The file was modified	`thys/Probabilistic_System_Zoo/Bool_Bounded_Set.thy` (diff)
The file was modified	`thys/Probabilistic_System_Zoo/Finitely_Bounded_Set_Counterexample.thy` (diff)
The file was modified	`thys/Probabilistic_System_Zoo/Nonempty_Bounded_Set.thy` (diff)
The file was modified	`thys/Probabilistic_System_Zoo/Probabilistic_Hierarchy.thy` (diff)
The file was modified	`thys/Probabilistic_System_Zoo/ROOT` (diff)
The file was modified	`thys/Probabilistic_While/Bernoulli.thy` (diff)
The file was modified	`thys/Probabilistic_While/ROOT` (diff)
The file was modified	`thys/Probabilistic_While/While_SPMF.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Interleave.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Misc.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Semantics.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/ThreadTracking.thy` (diff)
The file was modified	`thys/Promela/PromelaDatastructures.thy` (diff)
The file was modified	`thys/Promela/PromelaLTL.thy` (diff)
The file was modified	`thys/Promela/PromelaLTLConv.thy` (diff)
The file was modified	`thys/Promela/PromelaStatistics.thy` (diff)
The file was modified	`thys/Promela/ROOT` (diff)
The file was modified	`thys/Proof_Strategy_Language/Example.thy` (diff)
The file was modified	`thys/PropResPI/Prime_Implicates.thy` (diff)
The file was modified	`thys/PropResPI/Propositional_Resolution.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/CNF.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/CNF_To_Formula.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/Formulas.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/ROOT` (diff)
The file was modified	`thys/Propositional_Proof_Systems/Resolution.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/SC.thy` (diff)
The file was modified	`thys/PseudoHoops/Examples.thy` (diff)
The file was modified	`thys/PseudoHoops/LeftComplementedMonoid.thy` (diff)
The file was modified	`thys/Psi_Calculi/Chain.thy` (diff)
The file was modified	`thys/Ptolemys_Theorem/Ptolemys_Theorem.thy` (diff)
The file was modified	`thys/QR_Decomposition/Examples_QR_Abstract_Float.thy` (diff)
The file was modified	`thys/QR_Decomposition/Examples_QR_Abstract_Symbolic.thy` (diff)
The file was modified	`thys/QR_Decomposition/Examples_QR_IArrays_Float.thy` (diff)
The file was modified	`thys/QR_Decomposition/Examples_QR_IArrays_Symbolic.thy` (diff)
The file was modified	`thys/QR_Decomposition/Generalizations2.thy` (diff)
The file was modified	`thys/QR_Decomposition/IArray_Addenda_QR.thy` (diff)
The file was modified	`thys/QR_Decomposition/Matrix_To_IArray_QR.thy` (diff)
The file was modified	`thys/QR_Decomposition/Miscellaneous_QR.thy` (diff)
The file was modified	`thys/QR_Decomposition/ROOT` (diff)
The file was modified	`thys/Quick_Sort_Cost/ROOT` (diff)
The file was modified	`thys/Quick_Sort_Cost/Randomised_Quick_Sort.thy` (diff)
The file was modified	`thys/RIPEMD-160-SPARK/RIPEMD_160_SPARK.thy` (diff)
The file was modified	`thys/ROBDD/Abstract_Impl.thy` (diff)
The file was modified	`thys/ROBDD/Array_List.thy` (diff)
The file was modified	`thys/ROBDD/Option_Helpers.thy` (diff)
The file was modified	`thys/ROBDD/Pointer_Map_Impl.thy` (diff)
The file was modified	`thys/ROBDD/ROOT` (diff)
The file was modified	`thys/Ramsey-Infinite/Ramsey.thy` (diff)
The file was modified	`thys/Random_BSTs/ROOT` (diff)
The file was modified	`thys/Random_BSTs/Random_BSTs.thy` (diff)
The file was modified	`thys/Random_Graph_Subgraph_Threshold/Prob_Lemmas.thy` (diff)
The file was modified	`thys/Random_Graph_Subgraph_Threshold/Ugraph_Lemmas.thy` (diff)
The file was modified	`thys/Random_Graph_Subgraph_Threshold/Ugraph_Misc.thy` (diff)
The file was modified	`thys/Random_Graph_Subgraph_Threshold/Ugraph_Properties.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Lotteries.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Order_Predicates.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Preference_Profiles.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/ROOT` (diff)
The file was modified	`thys/Randomised_Social_Choice/Social_Decision_Schemes.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Stochastic_Dominance.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Utility_Functions.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Generalizations.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Miscellaneous.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Mod_Type.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/ROOT` (diff)
The file was modified	`thys/Real_Impl/Prime_Product.thy` (diff)
The file was modified	`thys/Real_Impl/ROOT` (diff)
The file was modified	`thys/Real_Impl/Real_Impl.thy` (diff)
The file was modified	`thys/Real_Impl/Real_Impl_Auxiliary.thy` (diff)
The file was modified	`thys/Real_Impl/Real_Unique_Impl.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Examples/Sepref_Dijkstra.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Examples/Sepref_Minitests.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Examples/Sepref_NDFS.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Examples/Sepref_WGraph.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Abs_Heap.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Abs_Heapmap.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Impl_Heap.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/IICF_Array_List.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/IICF_Array_Matrix.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/IICF_Indexed_Array_List.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/IICF_MS_Array_List.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/IICF_Sepl_Binding.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Intf/IICF_List.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Lib/PO_Normalizer.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Lib/Pf_Add.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Lib/Pf_Mono_Prover.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Lib/Sepref_Misc.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/ROOT` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Basic.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Constraints.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Foreach.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_ICF_Bindings.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Id_Op.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/benchmarks/Dijkstra/isabelle/Dijkstra_Benchmark.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/benchmarks/NestedDFS/isabelle/NDFS_Benchmark.thy` (diff)
The file was modified	`thys/Refine_Monadic/Generic/RefineG_While.thy` (diff)
The file was modified	`thys/Refine_Monadic/ROOT` (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_Mono_Prover.thy` (diff)
The file was modified	`thys/Refine_Monadic/examples/Examples.thy` (diff)
The file was modified	`thys/Refine_Monadic/examples/WordRefine.thy` (diff)
The file was modified	`thys/Regex_Equivalence/Automaton.thy` (diff)
The file was modified	`thys/Regex_Equivalence/Benchmark.thy` (diff)
The file was modified	`thys/Regex_Equivalence/Deriv_Autos.thy` (diff)
The file was modified	`thys/Regex_Equivalence/Derivatives_Finite.thy` (diff)
The file was modified	`thys/Regex_Equivalence/Examples.thy` (diff)
The file was modified	`thys/Regex_Equivalence/ROOT` (diff)
The file was modified	`thys/Regex_Equivalence/Regex_Equivalence.thy` (diff)
The file was modified	`thys/Regular-Sets/Equivalence_Checking.thy` (diff)
The file was modified	`thys/Regular-Sets/Equivalence_Checking2.thy` (diff)
The file was modified	`thys/Regular-Sets/Regexp_Constructions.thy` (diff)
The file was modified	`thys/Regular_Algebras/Dioid_Power_Sum.thy` (diff)
The file was modified	`thys/Regular_Algebras/Regular_Algebra_Models.thy` (diff)
The file was modified	`thys/Regular_Algebras/Regular_Algebras.thy` (diff)
The file was modified	`thys/Relation_Algebra/Relation_Algebra.thy` (diff)
The file was modified	`thys/Relation_Algebra/Relation_Algebra_Models.thy` (diff)
The file was modified	`thys/Rep_Fin_Groups/ROOT` (diff)
The file was modified	`thys/Rep_Fin_Groups/Rep_Fin_Groups.thy` (diff)
The file was modified	`thys/Residuated_Lattices/Action_Algebra.thy` (diff)
The file was modified	`thys/Residuated_Lattices/Action_Algebra_Models.thy` (diff)
The file was modified	`thys/Residuated_Lattices/Residuated_Lattices.thy` (diff)
The file was modified	`thys/Residuated_Lattices/Residuated_Relation_Algebra.thy` (diff)
The file was modified	`thys/Resolution_FOL/ROOT` (diff)
The file was modified	`thys/Resolution_FOL/TermsAndLiterals.thy` (diff)
The file was modified	`thys/Rewriting_Z/CL_Z.thy` (diff)
The file was modified	`thys/Rewriting_Z/Lambda_Z.thy` (diff)
The file was modified	`thys/Rewriting_Z/ROOT` (diff)
The file was modified	`thys/Rewriting_Z/Z.thy` (diff)
The file was modified	`thys/Ribbon_Proofs/More_Finite_Map.thy` (diff)
The file was modified	`thys/Ribbon_Proofs/Ribbons_Interfaces.thy` (diff)
The file was modified	`thys/Routing/IpRoute_Parser.thy` (diff)
The file was modified	`thys/Routing/Linux_Router.thy` (diff)
The file was modified	`thys/Routing/ROOT` (diff)
The file was modified	`thys/Routing/Routing_Table.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/SDS_Impossibility/SDS_Impossibility.thy` (diff)
The file was modified	`thys/SIFUM_Type_Systems/Preliminaries.thy` (diff)
The file was modified	`thys/SPARCv8/ROOT` (diff)
The file was modified	`thys/SPARCv8/SparcModel_MMU/Sparc_Execution.thy` (diff)
The file was modified	`thys/SPARCv8/SparcModel_MMU/Sparc_Instruction.thy` (diff)
The file was modified	`thys/SPARCv8/SparcModel_MMU/Sparc_State.thy` (diff)
The file was modified	`thys/SPARCv8/lib/Lib.thy` (diff)
The file was modified	`thys/SPARCv8/lib/WordDecl.thy` (diff)
The file was modified	`thys/Secondary_Sylow/GroupAction.thy` (diff)
The file was modified	`thys/Selection_Heap_Sort/Sort.thy` (diff)
The file was modified	`thys/Separata/ROOT` (diff)
The file was modified	`thys/Separata/Separata.thy` (diff)
The file was modified	`thys/Separation_Algebra/ex/Simple_Separation_Example.thy` (diff)
The file was modified	`thys/Separation_Algebra/ex/capDL/Types_D.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Assertions.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Examples/Hash_Table.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Examples/Idioms.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/ROOT` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Run.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Tools/Imperative_HOL_Add.thy` (diff)
The file was modified	`thys/SequentInvertibility/ModalSequents.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/ROOT` (diff)
The file was modified	`thys/SequentInvertibility/SRCTransforms.thy` (diff)
The file was modified	`thys/SequentInvertibility/SingleSuccedent.thy` (diff)
The file was modified	`thys/Shivers-CFA/AbsCFCorrect.thy` (diff)
The file was modified	`thys/Shivers-CFA/ROOT` (diff)
The file was modified	`thys/ShortestPath/ShortestPath.thy` (diff)
The file was modified	`thys/ShortestPath/ShortestPathNeg.thy` (diff)
The file was modified	`thys/Show/Old_Datatype/Old_Show_Examples.thy` (diff)
The file was modified	`thys/Show/Old_Datatype/Old_Show_Generator.thy` (diff)
The file was modified	`thys/Show/Old_Datatype/Old_Show_Instances.thy` (diff)
The file was modified	`thys/Show/Show.thy` (diff)
The file was modified	`thys/Show/Show_Complex.thy` (diff)
The file was modified	`thys/Show/Show_Instances.thy` (diff)
The file was modified	`thys/Show/Show_Poly.thy` (diff)
The file was modified	`thys/Show/Show_Real.thy` (diff)
The file was modified	`thys/Simpl/Generalise.thy` (diff)
The file was modified	`thys/Simpl/Language.thy` (diff)
The file was modified	`thys/Simpl/Simpl.thy` (diff)
The file was modified	`thys/Simpl/UserGuide.thy` (diff)
The file was modified	`thys/Simpl/Vcg.thy` (diff)
The file was modified	`thys/Simpl/ex/Quicksort.thy` (diff)
The file was modified	`thys/Simple_Firewall/Common/IP_Addr_WordInterval_toString.thy` (diff)
The file was modified	`thys/Simple_Firewall/Common/Lib_Enum_toString.thy` (diff)
The file was modified	`thys/Simple_Firewall/Primitives/Iface.thy` (diff)
The file was modified	`thys/Simple_Firewall/Primitives/L4_Protocol.thy` (diff)
The file was modified	`thys/Simple_Firewall/Primitives/Primitives_toString.thy` (diff)
The file was modified	`thys/Simple_Firewall/Service_Matrix.thy` (diff)
The file was modified	`thys/Simple_Firewall/SimpleFw_Semantics.thy` (diff)
The file was modified	`thys/Simple_Firewall/SimpleFw_Syntax.thy` (diff)
The file was modified	`thys/Skew_Heap/ROOT` (diff)
The file was modified	`thys/Skew_Heap/Skew_Heap.thy` (diff)
The file was modified	`thys/Slicing/JinjaVM/JVMCFG.thy` (diff)
The file was modified	`thys/Sort_Encodings/Preliminaries.thy` (diff)
The file was modified	`thys/Source_Coding_Theorem/Source_Coding_Theorem.thy` (diff)
The file was modified	`thys/Special_Function_Bounds/Atan_CF_Bounds.thy` (diff)
The file was modified	`thys/Special_Function_Bounds/Exp_Bounds.thy` (diff)
The file was modified	`thys/Special_Function_Bounds/Sqrt_Bounds.thy` (diff)
The file was modified	`thys/Splay_Tree/ROOT` (diff)
The file was modified	`thys/Splay_Tree/Splay_Heap.thy` (diff)
The file was modified	`thys/Splay_Tree/Splay_Tree.thy` (diff)
The file was modified	`thys/Sqrt_Babylonian/NthRoot_Impl.thy` (diff)
The file was modified	`thys/Sqrt_Babylonian/Sqrt_Babylonian_Auxiliary.thy` (diff)
The file was modified	`thys/Stable_Matching/Basis.thy` (diff)
The file was modified	`thys/Stable_Matching/Contracts.thy` (diff)
The file was modified	`thys/Statecharts/CarAudioSystem.thy` (diff)
The file was modified	`thys/Statecharts/Expr.thy` (diff)
The file was modified	`thys/Statecharts/HA.thy` (diff)
The file was modified	`thys/Statecharts/HAKripke.thy` (diff)
The file was modified	`thys/Stern_Brocot/Cotree.thy` (diff)
The file was modified	`thys/Stern_Brocot/ROOT` (diff)
The file was modified	`thys/Stern_Brocot/Stern_Brocot_Tree.thy` (diff)
The file was modified	`thys/Stewart_Apollonius/ROOT` (diff)
The file was modified	`thys/Stewart_Apollonius/Stewart_Apollonius.thy` (diff)
The file was modified	`thys/Stirling_Formula/Ln_Gamma_Asymptotics.thy` (diff)
The file was modified	`thys/Stirling_Formula/ROOT` (diff)
The file was modified	`thys/Stirling_Formula/Stirling_Formula.thy` (diff)
The file was modified	`thys/Stone_Kleene_Relation_Algebras/Iterings.thy` (diff)
The file was modified	`thys/Stone_Kleene_Relation_Algebras/Kleene_Relation_Algebras.thy` (diff)
The file was modified	`thys/Stone_Kleene_Relation_Algebras/Kleene_Relation_Subalgebras.thy` (diff)
The file was modified	`thys/Stone_Kleene_Relation_Algebras/Matrix_Kleene_Algebras.thy` (diff)
The file was modified	`thys/Stone_Relation_Algebras/Fixpoints.thy` (diff)
The file was modified	`thys/Stone_Relation_Algebras/Relation_Algebras.thy` (diff)
The file was modified	`thys/Stone_Relation_Algebras/Relation_Subalgebras.thy` (diff)
The file was modified	`thys/Stream-Fusion/LazyList.thy` (diff)
The file was modified	`thys/Stream_Fusion_Code/ROOT` (diff)
The file was modified	`thys/Stream_Fusion_Code/Stream_Fusion_LList.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Lib/Misc_Polynomial.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Sturm_Theorem.thy` (diff)
The file was modified	`thys/Sturm_Tarski/PolyMisc.thy` (diff)
The file was modified	`thys/Sturm_Tarski/ROOT` (diff)
The file was modified	`thys/Stuttering_Equivalence/PLTL.thy` (diff)
The file was modified	`thys/Stuttering_Equivalence/Samplers.thy` (diff)
The file was modified	`thys/Subresultants/Coeff_Int.thy` (diff)
The file was modified	`thys/Subresultants/Dichotomous_Lazard.thy` (diff)
The file was modified	`thys/Subresultants/More_Homomorphisms.thy` (diff)
The file was modified	`thys/Subresultants/ROOT` (diff)
The file was modified	`thys/Subresultants/Resultant_Prelim.thy` (diff)
The file was modified	`thys/Subresultants/Subresultant_Gcd.thy` (diff)
The file was modified	`thys/SumSquares/FourSquares.thy` (diff)
The file was modified	`thys/SumSquares/TwoSquares.thy` (diff)
The file was modified	`thys/SuperCalc/ROOT` (diff)
The file was modified	`thys/SuperCalc/equational_clausal_logic.thy` (diff)
The file was modified	`thys/SuperCalc/multisets_continued.thy` (diff)
The file was modified	`thys/SuperCalc/superposition.thy` (diff)
The file was modified	`thys/SuperCalc/terms.thy` (diff)
The file was modified	`thys/Surprise_Paradox/Surprise_Paradox.thy` (diff)
The file was modified	`thys/Tail_Recursive_Functions/CaseStudy2.thy` (diff)
The file was modified	`thys/Tail_Recursive_Functions/ROOT` (diff)
The file was modified	`thys/Tarskis_Geometry/Action.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/Hyperbolic_Tarski.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/Metric.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/Miscellany.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/ROOT` (diff)
The file was modified	`thys/Topology/LList_Topology.thy` (diff)
The file was modified	`thys/Topology/Topology.thy` (diff)
The file was modified	`thys/TortoiseHare/Basis.thy` (diff)
The file was modified	`thys/TortoiseHare/ROOT` (diff)
The file was modified	`thys/Transitive-Closure-II/ROOT` (diff)
The file was modified	`thys/Transitive-Closure-II/RTrancl.thy` (diff)
The file was modified	`thys/Transitive-Closure/RBT_Map_Set_Extension.thy` (diff)
The file was modified	`thys/Transitive-Closure/ROOT` (diff)
The file was modified	`thys/Tree-Automata/AbsAlgo.thy` (diff)
The file was modified	`thys/Tree-Automata/Ta.thy` (diff)
The file was modified	`thys/Tree-Automata/Ta_impl.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/Twelvefold_Way/Preliminaries.thy` (diff)
The file was modified	`thys/Twelvefold_Way/ROOT` (diff)
The file was modified	`thys/UPF_Firewall/PacketFilter/PolicyCore.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Imperative.thy` (diff)
The file was modified	`thys/UpDown_Scheme/ROOT` (diff)
The file was modified	`thys/Valuation/Valuation1.thy` (diff)
The file was modified	`thys/VectorSpace/FunctionLemmas.thy` (diff)
The file was modified	`thys/VectorSpace/LinearCombinations.thy` (diff)
The file was modified	`thys/VectorSpace/MonoidSums.thy` (diff)
The file was modified	`thys/VectorSpace/RingModuleFacts.thy` (diff)
The file was modified	`thys/VectorSpace/SumSpaces.thy` (diff)
The file was modified	`thys/VectorSpace/VectorSpace.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/CombinatorialAuctionCodeExtraction.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/MiscTools.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/RelationOperators.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/RelationProperties.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/UniformTieBreaking.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/Universes.thy` (diff)
The file was modified	`thys/WHATandWHERE_Security/MWLs.thy` (diff)
The file was modified	`thys/WHATandWHERE_Security/Type_System_example.thy` (diff)
The file was modified	`thys/WHATandWHERE_Security/Up_To_Technique.thy` (diff)
The file was modified	`thys/WHATandWHERE_Security/WHATWHERE_Security.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Almost_Full.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Higman_OI.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Minimal_Elements.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Multiset_Extension.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/ROOT` (diff)
The file was modified	`thys/Word_Lib/Enumeration.thy` (diff)
The file was modified	`thys/Word_Lib/Hex_Words.thy` (diff)
The file was modified	`thys/Word_Lib/More_Divides.thy` (diff)
The file was modified	`thys/Word_Lib/Norm_Words.thy` (diff)
The file was modified	`thys/Word_Lib/ROOT` (diff)
The file was modified	`thys/Word_Lib/Signed_Words.thy` (diff)
The file was modified	`thys/Word_Lib/WordBitwise_Signed.thy` (diff)
The file was modified	`thys/Word_Lib/Word_Lemmas.thy` (diff)
The file was modified	`thys/Word_Lib/Word_Syntax.thy` (diff)
The file was modified	`thys/XML/ROOT` (diff)
The file was modified	`thys/XML/Xml.thy` (diff)
The file was modified	`thys/XML/Xmlt.thy` (diff)
The file was modified	`thys/pGCL/Induction.thy` (diff)
The file was modified	`thys/pGCL/Misc.thy` (diff)
Changeset 8189:c3e3a3f090fa by wenzelm: clarified parent session, in order to disentangle imports;
The file was modified	`thys/ROBDD/ROOT` (diff)
Changeset 8188:a8a3f7e8797c by wenzelm: clarified imports;
The file was modified	`thys/Refine_Imperative_HOL/ROOT` (diff)
Changeset 8187:041dd26443b4 by wenzelm: clarified imports;
The file was modified	`thys/Algebraic_Numbers/ROOT` (diff)
The file was modified	`thys/Landau_Symbols/ROOT` (diff)
The file was modified	`thys/Refine_Imperative_HOL/ROOT` (diff)
Changeset 8186:2a4d0b3e37c0 by wenzelm: clarified imports;
The file was modified	`thys/Refine_Imperative_HOL/ROOT` (diff)