Changes

Summary

conversion of "op" syntax

Changeset 8674:3ccb204d9c5f by nipkow: conversion of "op" syntax
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/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/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/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/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/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/AWN/OClosed_Lifting.thy` (diff)
The file was modified	`thys/AWN/Toy.thy` (diff)
The file was modified	`thys/Abortable_Linearizable_Modules/Sequences.thy` (diff)
The file was modified	`thys/Abs_Int_ITP2012/Abs_Int3.thy` (diff)
The file was modified	`thys/Abstract-Rewriting/Relative_Rewriting.thy` (diff)
The file was modified	`thys/Abstract-Rewriting/SN_Order_Carrier.thy` (diff)
The file was modified	`thys/Abstract-Rewriting/SN_Orders.thy` (diff)
The file was modified	`thys/Abstract_Completeness/Abstract_Completeness.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Affine_Approximation.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Affine_Arithmetic_Auxiliarities.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Affine_Code.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Affine_Form.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Counterclockwise_2D_Arbitrary.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Counterclockwise_2D_Strict.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Executable_Euclidean_Space.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Floatarith_Expression.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Intersection.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Polygon.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Print.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Library.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Akra_Bazzi_Method.thy` (diff)
The file was modified	`thys/Akra_Bazzi/akra_bazzi.ML` (diff)
The file was modified	`thys/Algebraic_Numbers/Bivariate_Polynomials.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/Real_Algebraic_Numbers.thy` (diff)
The file was modified	`thys/Algebraic_Numbers/Real_Roots.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_Examples.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_dual_Examples.thy` (diff)
The file was modified	`thys/Algebraic_VCs/AVC_KAD/VC_KAD_scratch.thy` (diff)
The file was modified	`thys/Algebraic_VCs/AVC_KAD/VC_KAD_wf.thy` (diff)
The file was modified	`thys/Algebraic_VCs/AVC_KAD/VC_KAD_wf_Examples.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_Examples.thy` (diff)
The file was modified	`thys/Algebraic_VCs/AVC_KAT/VC_KAT_Examples2.thy` (diff)
The file was modified	`thys/Algebraic_VCs/AVC_KAT/VC_KAT_scratch.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/P2S2R.thy` (diff)
The file was modified	`thys/Algebraic_VCs/RKAT.thy` (diff)
The file was modified	`thys/Algebraic_VCs/RKAT_Models.thy` (diff)
The file was modified	`thys/Allen_Calculus/allen.thy` (diff)
The file was modified	`thys/Allen_Calculus/disjoint_relations.thy` (diff)
The file was modified	`thys/Allen_Calculus/examples.thy` (diff)
The file was modified	`thys/Allen_Calculus/jointly_exhaustive.thy` (diff)
The file was modified	`thys/Allen_Calculus/nest.thy` (diff)
The file was modified	`thys/Allen_Calculus/xor_cal.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Splay_Heap_Analysis.thy` (diff)
The file was modified	`thys/AnselmGod/AnselmGod.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_Functor.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Monoid.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_PMF.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_State.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Sum.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Test.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/Combinators.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Idiomatic_Terms.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Stream_Algebra.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Tree_Relabelling.thy` (diff)
The file was modified	`thys/AutoFocus-Stream/IL_AF_Stream.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Autoref_Bindings_HOL.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Digraph_Basic.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Indep_Vars.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Misc.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Mk_Term_Antiquot.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Mpat_Antiquot.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Refine_Util.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Select_Solve.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Lib/Tagged_Solver.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Parametricity/Param_HOL.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Parametricity/Relators.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Tool/Autoref_Fix_Rel.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Tool/Autoref_Id_Ops.thy` (diff)
The file was modified	`thys/Automatic_Refinement/Tool/Autoref_Phases.thy` (diff)
The file was modified	`thys/Bell_Numbers_Spivey/Bell_Numbers.thy` (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/Distinct_Degree_Factorization.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Factorize_Int_Poly.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/Polynomial_Record_Based.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Reconstruction.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Sublist_Iteration.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Unique_Factorization.thy` (diff)
The file was modified	`thys/Berlekamp_Zassenhaus/Unique_Factorization_Poly.thy` (diff)
The file was modified	`thys/Bernoulli/Bernoulli_Zeta.thy` (diff)
The file was modified	`thys/Bernoulli/Periodic_Bernpoly.thy` (diff)
The file was modified	`thys/Bertrands_Postulate/bertrand.ML` (diff)
The file was modified	`thys/Buchi_Complementation/Complementation.thy` (diff)
The file was modified	`thys/Buchi_Complementation/Complementation_Implement.thy` (diff)
The file was modified	`thys/Buchi_Complementation/Graph.thy` (diff)
The file was modified	`thys/Buchi_Complementation/Ranking.thy` (diff)
The file was modified	`thys/Buffons_Needle/Buffons_Needle.thy` (diff)
The file was modified	`thys/Buildings/Algebra.thy` (diff)
The file was modified	`thys/Buildings/Chamber.thy` (diff)
The file was modified	`thys/Buildings/Coxeter.thy` (diff)
The file was modified	`thys/Buildings/Prelim.thy` (diff)
The file was modified	`thys/Buildings/Simplicial.thy` (diff)
The file was modified	`thys/CAVA_Automata/Automata_Impl.thy` (diff)
The file was modified	`thys/CAVA_Automata/CAVA_Base/Code_String.thy` (diff)
The file was modified	`thys/CAVA_Automata/Digraph_Impl.thy` (diff)
The file was modified	`thys/CAVA_Automata/Lasso.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/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/CISC-Kernel/trace/Rushby-with-Control/Link_separation_kernel_model_to_CISK.thy` (diff)
The file was modified	`thys/CRDT/Convergence.thy` (diff)
The file was modified	`thys/CRDT/Counter.thy` (diff)
The file was modified	`thys/CRDT/ORSet.thy` (diff)
The file was modified	`thys/CRDT/RGA.thy` (diff)
The file was modified	`thys/CRDT/Util.thy` (diff)
The file was modified	`thys/Call_Arity/CoCallFix.thy` (diff)
The file was modified	`thys/Call_Arity/CoCallGraph-TTree.thy` (diff)
The file was modified	`thys/Call_Arity/CoCallGraph.thy` (diff)
The file was modified	`thys/Call_Arity/CoCallImplSafe.thy` (diff)
The file was modified	`thys/Call_Arity/Sestoft.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/TTree.thy` (diff)
The file was modified	`thys/Category/Cat.thy` (diff)
The file was modified	`thys/Category/HomFunctors.thy` (diff)
The file was modified	`thys/Category/Yoneda.thy` (diff)
The file was modified	`thys/Cayley_Hamilton/Cayley_Hamilton.thy` (diff)
The file was modified	`thys/Chord_Segments/Chord_Segments.thy` (diff)
The file was modified	`thys/Circus/Circus_Syntax.thy` (diff)
The file was modified	`thys/Circus/Denotational_Semantics.thy` (diff)
The file was modified	`thys/ClockSynchInst/LynchInstance.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/LList_CCPO_Topology.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/TLList.thy` (diff)
The file was modified	`thys/Coinductive/TLList_CCPO.thy` (diff)
The file was modified	`thys/Coinductive_Languages/Coinductive_Language.thy` (diff)
The file was modified	`thys/Coinductive_Languages/Context_Free_Grammar.thy` (diff)
The file was modified	`thys/Collections/Examples/Autoref/Coll_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/ICF/PerformanceTest.thy` (diff)
The file was modified	`thys/Collections/Examples/Refine_Monadic/Foreach_Refine.thy` (diff)
The file was modified	`thys/Collections/GenCF/Gen/Gen_Comp.thy` (diff)
The file was modified	`thys/Collections/GenCF/Gen/Gen_Map.thy` (diff)
The file was modified	`thys/Collections/GenCF/Gen/Gen_Map2Set.thy` (diff)
The file was modified	`thys/Collections/GenCF/Gen/Gen_Set.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_Bit_Set.thy` (diff)
The file was modified	`thys/Collections/GenCF/Impl/Impl_Cfun_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_List_Set.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/CollectionsV1.thy` (diff)
The file was modified	`thys/Collections/ICF/ICF_Autoref.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/MapGA.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/SetGA.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/ArrayHashMap_Impl.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/HashMap_Impl.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/ListSetImpl_Invar.thy` (diff)
The file was modified	`thys/Collections/ICF/tools/Ord_Code_Preproc.thy` (diff)
The file was modified	`thys/Collections/Iterator/Array_Iterator.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/SetIterator.thy` (diff)
The file was modified	`thys/Collections/Lib/HashCode.thy` (diff)
The file was modified	`thys/Collections/Userguides/ICF_Userguide.thy` (diff)
The file was modified	`thys/Collections/Userguides/Refine_Monadic_Userguide.thy` (diff)
The file was modified	`thys/Comparison_Sort_Lower_Bound/Linorder_Relations.thy` (diff)
The file was modified	`thys/Complx/OG_Soundness.thy` (diff)
The file was modified	`thys/Complx/OG_Syntax.thy` (diff)
The file was modified	`thys/Complx/lib/Cache_Tactics.thy` (diff)
The file was modified	`thys/ConcurrentGC/Model.thy` (diff)
The file was modified	`thys/ConcurrentIMP/CIMP_one_place_buffer_ex.thy` (diff)
The file was modified	`thys/ConcurrentIMP/CIMP_pred.thy` (diff)
The file was modified	`thys/ConcurrentIMP/CIMP_unbounded_buffer_ex.thy` (diff)
The file was modified	`thys/ConcurrentIMP/CIMP_vcg.thy` (diff)
The file was modified	`thys/Concurrent_Ref_Alg/Conjunctive_Sequential.thy` (diff)
The file was modified	`thys/Concurrent_Ref_Alg/Infimum_Nat.thy` (diff)
The file was modified	`thys/Consensus_Refined/Refinement.thy` (diff)
The file was modified	`thys/Consensus_Refined/Voting.thy` (diff)
The file was modified	`thys/Constructor_Funs/Constructor_Funs.thy` (diff)
The file was modified	`thys/Constructor_Funs/Test_Constructor_Funs.thy` (diff)
The file was modified	`thys/Containers/AssocList.thy` (diff)
The file was modified	`thys/Containers/Closure_Set.thy` (diff)
The file was modified	`thys/Containers/Collection_Eq.thy` (diff)
The file was modified	`thys/Containers/Containers_Auxiliary.thy` (diff)
The file was modified	`thys/Containers/Containers_Userguide.thy` (diff)
The file was modified	`thys/Containers/DList_Set.thy` (diff)
The file was modified	`thys/Containers/Equal.thy` (diff)
The file was modified	`thys/Containers/ITP-2013/Benchmark_Bool.thy` (diff)
The file was modified	`thys/Containers/ITP-2013/Benchmark_Set_LC.thy` (diff)
The file was modified	`thys/Containers/List_Fusion.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_ext.thy` (diff)
The file was modified	`thys/Containers/Set_Impl.thy` (diff)
The file was modified	`thys/Containers/Set_Linorder.thy` (diff)
The file was modified	`thys/Count_Complex_Roots/Count_Complex_Roots.thy` (diff)
The file was modified	`thys/Count_Complex_Roots/Count_Complex_Roots_Examples.thy` (diff)
The file was modified	`thys/Count_Complex_Roots/Extended_Sturm.thy` (diff)
The file was modified	`thys/CryptHOL/Computational_Model.thy` (diff)
The file was modified	`thys/CryptHOL/Cyclic_Group.thy` (diff)
The file was modified	`thys/CryptHOL/Environment_Functor.thy` (diff)
The file was modified	`thys/CryptHOL/GPV_Applicative.thy` (diff)
The file was modified	`thys/CryptHOL/GPV_Bisim.thy` (diff)
The file was modified	`thys/CryptHOL/GPV_Expectation.thy` (diff)
The file was modified	`thys/CryptHOL/Generat.thy` (diff)
The file was modified	`thys/CryptHOL/Generative_Probabilistic_Value.thy` (diff)
The file was modified	`thys/CryptHOL/List_Bits.thy` (diff)
The file was modified	`thys/CryptHOL/Misc_CryptHOL.thy` (diff)
The file was modified	`thys/CryptHOL/Partial_Function_Set.thy` (diff)
The file was modified	`thys/CryptHOL/Resumption.thy` (diff)
The file was modified	`thys/CryptHOL/SPMF_Applicative.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/Nested_DFS.thy` (diff)
The file was modified	`thys/DFS_Framework/Examples/Reachable_Nodes.thy` (diff)
The file was modified	`thys/DFS_Framework/Examples/Tarjan.thy` (diff)
The file was modified	`thys/DFS_Framework/Misc/Impl_Rev_Array_Stack.thy` (diff)
The file was modified	`thys/Datatype_Order_Generator/Order_Generator.thy` (diff)
The file was modified	`thys/Datatype_Order_Generator/hash_generator.ML` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/BigStepLam.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/ChangeEnv.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/DeclSemAsDenot.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/DeclSemAsDenotFSet.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/DeclSemAsNDInterpFSet.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/DenotCompleteFSet.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/DenotCongruenceFSet.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/DenotEqualitiesFSet.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/DenotLam5.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/DenotSoundFSet.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/EquivDenotInterTypes.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/EquivRelationalDenotFSet.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/InterTypeSystem.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/MutableRef.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/MutableRefProps.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/Optimizer.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/RelationalSemFSet.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/SmallStepLam.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/SystemF.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/ValueProps.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/Values.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/ValuesFSet.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/ValuesFSetProps.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/Deep_Learning/DL_Deep_Model.thy` (diff)
The file was modified	`thys/Deep_Learning/PP_More_List2.thy` (diff)
The file was modified	`thys/Deep_Learning/PP_Poly_Mapping.thy` (diff)
The file was modified	`thys/Deep_Learning/Tensor.thy` (diff)
The file was modified	`thys/Deep_Learning/Tensor_Plus.thy` (diff)
The file was modified	`thys/Deep_Learning/Tensor_Scalar_Mult.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Compiler_Pred.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Semantics.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Transformations.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Refinement/CompositionalRefinement.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Refinement/Examples/Eg1Eg2.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/Dependent_SIFUM_Type_Systems/Language.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Type_Systems/LocallySoundModeUse.thy` (diff)
The file was modified	`thys/Deriving/Comparator_Generator/Comparator.thy` (diff)
The file was modified	`thys/Deriving/Comparator_Generator/Compare.thy` (diff)
The file was modified	`thys/Deriving/Comparator_Generator/Compare_Order_Instances.thy` (diff)
The file was modified	`thys/Deriving/Derive_Examples.thy` (diff)
The file was modified	`thys/Deriving/Equality_Generator/Equality_Generator.thy` (diff)
The file was modified	`thys/Deriving/Equality_Generator/Equality_Instances.thy` (diff)
The file was modified	`thys/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/Impossibility.thy` (diff)
The file was modified	`thys/Dict_Construction/Introduction.thy` (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_Dynamic_Logic.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Proof_Checker.thy` (diff)
The file was modified	`thys/Differential_Dynamic_Logic/Syntax.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/Dijkstra_Shortest_Path/Dijkstra_Impl_Adet.thy` (diff)
The file was modified	`thys/Dijkstra_Shortest_Path/GraphGA.thy` (diff)
The file was modified	`thys/Diophantine_Eqns_Lin_Hom/Algorithm.thy` (diff)
The file was modified	`thys/Diophantine_Eqns_Lin_Hom/List_Vector.thy` (diff)
The file was modified	`thys/Diophantine_Eqns_Lin_Hom/Simple_Algorithm.thy` (diff)
The file was modified	`thys/Diophantine_Eqns_Lin_Hom/Sorted_Wrt.thy` (diff)
The file was modified	`thys/Dirichlet_Series/Dirichlet_Efficient_Code.thy` (diff)
The file was modified	`thys/Dirichlet_Series/Dirichlet_Misc.thy` (diff)
The file was modified	`thys/Dirichlet_Series/Dirichlet_Product.thy` (diff)
The file was modified	`thys/Dirichlet_Series/Dirichlet_Series_Analysis.thy` (diff)
The file was modified	`thys/Dirichlet_Series/More_Totient.thy` (diff)
The file was modified	`thys/DynamicArchitectures/Configuration_Traces.thy` (diff)
The file was modified	`thys/DynamicArchitectures/Dynamic_Architecture_Calculus.thy` (diff)
The file was modified	`thys/E_Transcendental/E_Transcendental.thy` (diff)
The file was modified	`thys/Echelon_Form/Echelon_Form_IArrays.thy` (diff)
The file was modified	`thys/EdmondsKarp_Maxflow/EdmondsKarp_Termination_Abstract.thy` (diff)
The file was modified	`thys/Efficient-Mergesort/Efficient_Sort.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Invariants.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Measure_Preserving_Transformations.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/FFT/FFT.thy` (diff)
The file was modified	`thys/FLP/FLPExistingSystem.thy` (diff)
The file was modified	`thys/FOL-Fitting/FOL_Fitting.thy` (diff)
The file was modified	`thys/Featherweight_OCL/UML_Library.thy` (diff)
The file was modified	`thys/Featherweight_OCL/UML_Logic.thy` (diff)
The file was modified	`thys/Featherweight_OCL/basic_types/UML_Integer.thy` (diff)
The file was modified	`thys/Featherweight_OCL/basic_types/UML_Real.thy` (diff)
The file was modified	`thys/Featherweight_OCL/basic_types/UML_String.thy` (diff)
The file was modified	`thys/FinFun/FinFun.thy` (diff)
The file was modified	`thys/FinFun/FinFunPred.thy` (diff)
The file was modified	`thys/Finger-Trees/FingerTree.thy` (diff)
The file was modified	`thys/First_Welfare_Theorem/Consumers.thy` (diff)
The file was modified	`thys/First_Welfare_Theorem/Exchange_Economy.thy` (diff)
The file was modified	`thys/First_Welfare_Theorem/Preferences.thy` (diff)
The file was modified	`thys/First_Welfare_Theorem/Private_Ownership_Economy.thy` (diff)
The file was modified	`thys/First_Welfare_Theorem/Utility_Functions.thy` (diff)
The file was modified	`thys/Fisher_Yates/Fisher_Yates.thy` (diff)
The file was modified	`thys/Floyd_Warshall/FW_Code.thy` (diff)
The file was modified	`thys/Floyd_Warshall/Floyd_Warshall.thy` (diff)
The file was modified	`thys/Floyd_Warshall/Recursion_Combinators.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/ArchCompAux.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/ArchCompProps.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/ArchStat.thy` (diff)
The file was modified	`thys/Flyspeck-Tame/PlaneGraphIso.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_code.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/SSA_CFG.thy` (diff)
The file was modified	`thys/Formal_SSA/SSA_CFG_code.thy` (diff)
The file was modified	`thys/Formal_SSA/SSA_Transfer_Rules.thy` (diff)
The file was modified	`thys/Formal_SSA/WhileGraphSSA.thy` (diff)
The file was modified	`thys/Formula_Derivatives/Automaton.thy` (diff)
The file was modified	`thys/Formula_Derivatives/Presburger_Formula.thy` (diff)
The file was modified	`thys/Formula_Derivatives/WS1S_Alt_Formula.thy` (diff)
The file was modified	`thys/Formula_Derivatives/WS1S_Formula.thy` (diff)
The file was modified	`thys/Formula_Derivatives/WS1S_Nameful.thy` (diff)
The file was modified	`thys/Formula_Derivatives/WS1S_Presburger_Equivalence.thy` (diff)
The file was modified	`thys/Free-Groups/C2.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/Gabow_SCC/Gabow_GBG.thy` (diff)
The file was modified	`thys/Gabow_SCC/Gabow_Skeleton.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/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/RP_RF.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/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/Linear_Maps.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Matrix_To_IArray.thy` (diff)
The file was modified	`thys/Graph_Theory/Funpow.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/Group-Ring-Module/Algebra1.thy` (diff)
The file was modified	`thys/Group-Ring-Module/Algebra2.thy` (diff)
The file was modified	`thys/Group-Ring-Module/Algebra4.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/Data_Integer.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/Data_List.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/Data_Maybe.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/Data_Tuple.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/HOLCF_Prelude.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/List_Comprehension.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/Num_Class.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/Numeral_Cpo.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/examples/Fibs.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/examples/GHC_Rewrite_Rules.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/examples/HLint.thy` (diff)
The file was modified	`thys/HOLCF-Prelude/examples/Sieve_Primes.thy` (diff)
The file was modified	`thys/HereditarilyFinite/OrdArith.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/Cars.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/Length.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/Move.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/NatInt.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/Restriction.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/Sensors.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/Traffic.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/Views.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/perfect/HMLSL_Perfect.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/perfect/Perfect_Sensors.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/perfect/Safety_Perfect.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/regular/HMLSL_Regular.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/regular/Regular_Sensors.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/regular/Safety_Regular.thy` (diff)
The file was modified	`thys/IEEE_Floating_Point/Code_Float.thy` (diff)
The file was modified	`thys/IEEE_Floating_Point/Conversion_IEEE_Float.thy` (diff)
The file was modified	`thys/IMAP-CRDT/IMAP-def.thy` (diff)
The file was modified	`thys/IMAP-CRDT/IMAP-proof-commute.thy` (diff)
The file was modified	`thys/IMAP-CRDT/IMAP-proof-helpers.thy` (diff)
The file was modified	`thys/IP_Addresses/Prefix_Match_toString.thy` (diff)
The file was modified	`thys/IP_Addresses/WordInterval_Sorted.thy` (diff)
The file was modified	`thys/Incompleteness/SyntaxN.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Abstract_Rules_To_Incredible.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Build_Incredible_Tree.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Entailment.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Incredible_Completeness.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Incredible_Correctness.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_Propositional_Tasks.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Incredible_Signatures.thy` (diff)
The file was modified	`thys/Incredible_Proof_Machine/Indexed_FSet.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/Rose_Tree.thy` (diff)
The file was modified	`thys/InfPathElimination/Conf.thy` (diff)
The file was modified	`thys/InfPathElimination/LTS.thy` (diff)
The file was modified	`thys/InfPathElimination/Labels.thy` (diff)
The file was modified	`thys/InfPathElimination/RB.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Access_Matrix_Embeddings.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Common/Negation_Type_DNF.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Common/Repeat_Stabilize.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Common/Word_Upto.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/Small_Examples.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Examples/containern/Analyze_Containern.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/No_Spoof_Embeddings.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Common_Primitive_Lemmas.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Interface_Replace.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Interfaces_Normalize.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Primitive_Abstract.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Transform.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Ternary/MatchExpr_Fold.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/meta_isabelle/Parser_init.thy` (diff)
The file was modified	`thys/Jinja/BV/BVExample.thy` (diff)
The file was modified	`thys/Jinja/BV/TF_JVM.thy` (diff)
The file was modified	`thys/Jinja/DFA/Listn.thy` (diff)
The file was modified	`thys/JinjaThreads/BV/TF_JVM.thy` (diff)
The file was modified	`thys/JinjaThreads/Basic/Auxiliary.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/Value.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/Correctness.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/Correctness1Threaded.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/Exception_Tables.thy` (diff)
The file was modified	`thys/JinjaThreads/DFA/Listn.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/HB_Completion.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Compiler.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Framework.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Spec.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/JMM_Type2.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/SC_Legal.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/CompositionSeries.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/JordanHolder.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/DL_Missing_Matrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Determinant.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gauss_Jordan_Elimination.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Gram_Schmidt.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form_Existence.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form_Uniqueness.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Comparison.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Complexity.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_IArray_Impl.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix_Kernel.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Spectral_Radius.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Strassen_Algorithm_Code.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/VS_Connect.thy` (diff)
The file was modified	`thys/KAD/Antidomain_Semiring.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/Range_Semiring.thy` (diff)
The file was modified	`thys/KAT_and_DRA/SingleSorted/DRA_Models.thy` (diff)
The file was modified	`thys/KAT_and_DRA/SingleSorted/KAT_Models.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/AuthenticationI.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/IK.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Implem.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Implem_asymmetric.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Implem_lemmas.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Implem_symmetric.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Message_derivation.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Messages.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Payloads.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/Refinement.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl1.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl3.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/dhlvl3_asymmetric.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl1.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl3_asymmetric.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/pfslvl3_symmetric.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl1.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl3.thy` (diff)
The file was modified	`thys/Key_Agreement_Strong_Adversaries/sklvl3_symmetric.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Dioid.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Dioid_Models.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Kleene_Algebra.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Kleene_Algebra_Models.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Omega_Algebra_Models.thy` (diff)
The file was modified	`thys/LOFT/LinuxRouter_OpenFlow_Translation.thy` (diff)
The file was modified	`thys/LOFT/List_Group.thy` (diff)
The file was modified	`thys/LOFT/OpenFlow_Action.thy` (diff)
The file was modified	`thys/LOFT/OpenFlow_Helpers.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/LOFT/Sort_Descending.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/DTS.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/LTL_FGXU.thy` (diff)
The file was modified	`thys/LTL_to_GBA/LTL_to_GBA_impl.thy` (diff)
The file was modified	`thys/LambdaMu/ContextFacts.thy` (diff)
The file was modified	`thys/LambdaMu/DeBruijn.thy` (diff)
The file was modified	`thys/LambdaMu/Peirce.thy` (diff)
The file was modified	`thys/LambdaMu/Progress.thy` (diff)
The file was modified	`thys/LambdaMu/Reduction.thy` (diff)
The file was modified	`thys/LambdaMu/Substitution.thy` (diff)
The file was modified	`thys/LambdaMu/TypePreservation.thy` (diff)
The file was modified	`thys/Lambda_Free_KBOs/Lambda_Free_KBO_App.thy` (diff)
The file was modified	`thys/Lambda_Free_KBOs/Lambda_Free_KBO_Basic.thy` (diff)
The file was modified	`thys/Lambda_Free_KBOs/Lambda_Free_KBO_Std.thy` (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_RPOs/Lambda_Free_RPO_App.thy` (diff)
The file was modified	`thys/Lambda_Free_RPOs/Lambda_Free_RPO_Optim.thy` (diff)
The file was modified	`thys/Lambda_Free_RPOs/Lambda_Free_RPO_Std.thy` (diff)
The file was modified	`thys/Lambda_Free_RPOs/Lambda_Free_Term.thy` (diff)
The file was modified	`thys/Landau_Symbols/Group_Sort.thy` (diff)
The file was modified	`thys/Landau_Symbols/Landau_More.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/LatticeProperties/Conj_Disj.thy` (diff)
The file was modified	`thys/LatticeProperties/Modular_Distrib_Lattice.thy` (diff)
The file was modified	`thys/Launchbury/ValueSimilarity.thy` (diff)
The file was modified	`thys/Lazy_Case/Lazy_Case.thy` (diff)
The file was modified	`thys/Lazy_Case/Test_Lazy_Case.thy` (diff)
The file was modified	`thys/LightweightJava/Lightweight_Java_Equivalence.thy` (diff)
The file was modified	`thys/LightweightJava/Lightweight_Java_Proof.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Linear_Homogenous_Recurrences.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Linear_Inhomogenous_Recurrences.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Linear_Recurrences_Common.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Linear_Recurrences_Misc.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Linear_Recurrences_Pretty.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Linear_Recurrences_Solver.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Linear_Recurrences_Test.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Partial_Fraction_Decomposition.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Pochhammer_Polynomials.thy` (diff)
The file was modified	`thys/Linear_Recurrences/RatFPS.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Rational_FPS_Solver.thy` (diff)
The file was modified	`thys/Linear_Recurrences/Show_RatFPS.thy` (diff)
The file was modified	`thys/List-Index/List_Index.thy` (diff)
The file was modified	`thys/List-Infinite/CommonSet/SetInterval2.thy` (diff)
The file was modified	`thys/List-Infinite/CommonSet/SetIntervalCut.thy` (diff)
The file was modified	`thys/List-Infinite/CommonSet/SetIntervalStep.thy` (diff)
The file was modified	`thys/List-Infinite/ListInf/List2.thy` (diff)
The file was modified	`thys/List-Infinite/ListInf/ListInf_Prefix.thy` (diff)
The file was modified	`thys/List_Update/BIT.thy` (diff)
The file was modified	`thys/List_Update/Bit_Strings.thy` (diff)
The file was modified	`thys/List_Update/Comb.thy` (diff)
The file was modified	`thys/LocalLexing/InductRules.thy` (diff)
The file was modified	`thys/LocalLexing/Limit.thy` (diff)
The file was modified	`thys/LocalLexing/ListTools.thy` (diff)
The file was modified	`thys/LocalLexing/LocalLexing.thy` (diff)
The file was modified	`thys/LocalLexing/LocalLexingLemmas.thy` (diff)
The file was modified	`thys/LocalLexing/MainTheorems.thy` (diff)
The file was modified	`thys/LocalLexing/PathLemmas.thy` (diff)
The file was modified	`thys/LocalLexing/TheoremD11.thy` (diff)
The file was modified	`thys/LocalLexing/TheoremD12.thy` (diff)
The file was modified	`thys/LocalLexing/TheoremD13.thy` (diff)
The file was modified	`thys/LocalLexing/TheoremD5.thy` (diff)
The file was modified	`thys/LocalLexing/TheoremD9.thy` (diff)
The file was modified	`thys/Locally-Nameless-Sigma/Sigma/Sigma.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/Matrix_For_Marginals.thy` (diff)
The file was modified	`thys/MFMC_Countable/Max_Flow_Min_Cut_Countable.thy` (diff)
The file was modified	`thys/MFMC_Countable/Rel_PMF_Characterisation.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/M2L.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/WS1S.thy` (diff)
The file was modified	`thys/Markov_Models/Classifying_Markov_Chain_States.thy` (diff)
The file was modified	`thys/Markov_Models/Continuous_Time_Markov_Chain.thy` (diff)
The file was modified	`thys/Markov_Models/Discrete_Time_Markov_Chain.thy` (diff)
The file was modified	`thys/Markov_Models/Discrete_Time_Markov_Process.thy` (diff)
The file was modified	`thys/Markov_Models/MDP_Reachability_Problem.thy` (diff)
The file was modified	`thys/Markov_Models/Markov_Decision_Process.thy` (diff)
The file was modified	`thys/Markov_Models/Markov_Models_Auxiliary.thy` (diff)
The file was modified	`thys/Markov_Models/Trace_Space_Equals_Markov_Processes.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Crowds_Protocol.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Gossip_Broadcast.thy` (diff)
The file was modified	`thys/Markov_Models/ex/MDP_RP.thy` (diff)
The file was modified	`thys/Markov_Models/ex/MDP_RP_Certification.thy` (diff)
The file was modified	`thys/Matrix/Matrix_Legacy.thy` (diff)
The file was modified	`thys/Matrix/Ordered_Semiring.thy` (diff)
The file was modified	`thys/Menger/DisjointPaths.thy` (diff)
The file was modified	`thys/Menger/Helpers.thy` (diff)
The file was modified	`thys/Menger/Separations.thy` (diff)
The file was modified	`thys/Minkowskis_Theorem/Minkowskis_Theorem.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/FL_Formula.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/FL_Transition_System.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/FL_Validity.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/FS_Set.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/Formula.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/L_Transform.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/Residual.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/Transition_System.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/Validity.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/Weak_Transition_System.thy` (diff)
The file was modified	`thys/Monad_Normalisation/Monad_Normalisation.thy` (diff)
The file was modified	`thys/Monad_Normalisation/Monad_Normalisation_Test.thy` (diff)
The file was modified	`thys/MonoBoolTranAlgebra/Mono_Bool_Tran.thy` (diff)
The file was modified	`thys/MonoBoolTranAlgebra/Mono_Bool_Tran_Algebra.thy` (diff)
The file was modified	`thys/Monomorphic_Monad/Interpreter.thy` (diff)
The file was modified	`thys/Monomorphic_Monad/Just_Do_It_Examples.thy` (diff)
The file was modified	`thys/Monomorphic_Monad/Monad_Overloading.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/Multirelations.thy` (diff)
The file was modified	`thys/Myhill-Nerode/Closures.thy` (diff)
The file was modified	`thys/Myhill-Nerode/Non_Regular_Languages.thy` (diff)
The file was modified	`thys/Name_Carrying_Type_Inference/Fresh.thy` (diff)
The file was modified	`thys/Name_Carrying_Type_Inference/Permutation.thy` (diff)
The file was modified	`thys/Name_Carrying_Type_Inference/SimplyTyped.thy` (diff)
The file was modified	`thys/Nat-Interval-Logic/IL_Interval.thy` (diff)
The file was modified	`thys/Nat-Interval-Logic/IL_IntervalOperators.thy` (diff)
The file was modified	`thys/Native_Word/Bits_Integer.thy` (diff)
The file was modified	`thys/Native_Word/Native_Cast.thy` (diff)
The file was modified	`thys/Native_Word/Native_Word_Imperative_HOL.thy` (diff)
The file was modified	`thys/Native_Word/Uint.thy` (diff)
The file was modified	`thys/Native_Word/Uint16.thy` (diff)
The file was modified	`thys/Native_Word/Uint32.thy` (diff)
The file was modified	`thys/Native_Word/Uint64.thy` (diff)
The file was modified	`thys/Native_Word/Uint8.thy` (diff)
The file was modified	`thys/Native_Word/Word_Misc.thy` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/Goodstein_Sequence.thy` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/Hereditary_Multiset.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/Signed_Hereditary_Multiset.thy` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/Signed_Multiset.thy` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/Syntactic_Ordinal.thy` (diff)
The file was modified	`thys/Nested_Multisets_Ordinals/Unary_PCF.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Tainting/MeasrDroid.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/Analysis_Tainting.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_BLPbasic.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_BLPstrict.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Security_Invariants/SINVAR_Tainting.thy` (diff)
The file was modified	`thys/No_FTL_observers/Axioms.thy` (diff)
The file was modified	`thys/No_FTL_observers/SomeFunc.thy` (diff)
The file was modified	`thys/No_FTL_observers/SpaceTime.thy` (diff)
The file was modified	`thys/Nominal2/Nominal2.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/nominal_dt_alpha.ML` (diff)
The file was modified	`thys/Nominal2/nominal_library.ML` (diff)
The file was modified	`thys/Noninterference_Concurrent_Composition/ConcurrentComposition.thy` (diff)
The file was modified	`thys/Noninterference_Sequential_Composition/SequentialComposition.thy` (diff)
The file was modified	`thys/NormByEval/NBE.thy` (diff)
The file was modified	`thys/Open_Induction/Open_Induction.thy` (diff)
The file was modified	`thys/Open_Induction/Restricted_Predicates.thy` (diff)
The file was modified	`thys/Optics/Interp.thy` (diff)
The file was modified	`thys/Optics/Lens_Algebra.thy` (diff)
The file was modified	`thys/Optics/Lens_Instances.thy` (diff)
The file was modified	`thys/Optics/Lens_Laws.thy` (diff)
The file was modified	`thys/Optics/Lens_Order.thy` (diff)
The file was modified	`thys/Optics/Lens_State.thy` (diff)
The file was modified	`thys/Optics/Lenses.thy` (diff)
The file was modified	`thys/Optics/Prisms.thy` (diff)
The file was modified	`thys/Optics/Two.thy` (diff)
The file was modified	`thys/Orbit_Stabiliser/Left_Coset.thy` (diff)
The file was modified	`thys/Orbit_Stabiliser/Orbit_Stabiliser.thy` (diff)
The file was modified	`thys/Orbit_Stabiliser/Tetrahedron.thy` (diff)
The file was modified	`thys/Ordinal/OrdinalArith.thy` (diff)
The file was modified	`thys/Ordinal/OrdinalInverse.thy` (diff)
The file was modified	`thys/Ordinal/OrdinalOmega.thy` (diff)
The file was modified	`thys/Ordinal/OrdinalRec.thy` (diff)
The file was modified	`thys/Ordinal/OrdinalVeblen.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Examples_Integral.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Examples_One_Step_Method.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Examples_Poincare_Map.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_C0.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_C1.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Ex/Lorenz/Result_Elements.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Cones.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Flow.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Initial_Value_Problem.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Picard_Lindeloef_Qualitative.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Poincare_Map.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/IVP/Upper_Lower_Solution.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Library/Bounded_Linear_Operator.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.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/Refine_Vector_List.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/ODE_Auxiliarities.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Refinement/Autoref_Misc.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Refinement/Refine_Folds.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Refinement/Refine_String.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Refinement/Weak_Set.thy` (diff)
The file was modified	`thys/PLM/TAO_1_Embedding.thy` (diff)
The file was modified	`thys/PLM/TAO_6_Identifiable.thy` (diff)
The file was modified	`thys/PSemigroupsConvolution/Binary_Modalities.thy` (diff)
The file was modified	`thys/PSemigroupsConvolution/Partial_Semigroup_Lifting.thy` (diff)
The file was modified	`thys/Perfect-Number-Thm/Sigma.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Check_Matrix_Growth.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/Perron_Frobenius_Aux.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Perron_Frobenius_General.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Perron_Frobenius_Irreducible.thy` (diff)
The file was modified	`thys/Perron_Frobenius/Spectral_Radius_Theory_2.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/Planar_Complete.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Planar_Subdivision.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Planar_Subgraph.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Gauss_Lemma.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Missing_List.thy` (diff)
The file was modified	`thys/Polynomial_Factorization/Missing_Polynomial_Factorial.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Improved_Code_Equations.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Polynomial.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Ring_Hom_Poly.thy` (diff)
The file was modified	`thys/Polynomials/Abstract_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/Power_Products.thy` (diff)
The file was modified	`thys/Polynomials/Show_Polynomials.thy` (diff)
The file was modified	`thys/Posix-Lexing/Lexer.thy` (diff)
The file was modified	`thys/Posix-Lexing/Simplifying.thy` (diff)
The file was modified	`thys/Possibilistic_Noninterference/Concrete.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/Prime_Harmonic_Series/Prime_Harmonic.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Concrete.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Language_Semantics.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/Vardi.thy` (diff)
The file was modified	`thys/Probabilistic_System_Zoo/Vardi_Counterexample.thy` (diff)
The file was modified	`thys/Probabilistic_While/Bernoulli.thy` (diff)
The file was modified	`thys/Probabilistic_While/Fast_Dice_Roll.thy` (diff)
The file was modified	`thys/Probabilistic_While/Geometric.thy` (diff)
The file was modified	`thys/Probabilistic_While/While_SPMF.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/AcquisitionHistory.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/ConsInterleave.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Interleave.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Misc.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Normalization.thy` (diff)
The file was modified	`thys/Promela/Promela.thy` (diff)
The file was modified	`thys/Promela/PromelaInvariants.thy` (diff)
The file was modified	`thys/Proof_Strategy_Language/Example.thy` (diff)
The file was modified	`thys/Proof_Strategy_Language/PSL.thy` (diff)
The file was modified	`thys/Proof_Strategy_Language/Try_Hard.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/CNF.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/CNF_Formulas.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/CNF_Formulas_Sema.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/CNF_Sema.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/CNF_To_Formula.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/Compactness.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/Consistency.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/HCSCND.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/HC_Compl_Consistency.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/LSC.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/LSC_Resolution.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/MiniFormulas.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/MiniFormulas_Sema.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/MiniSC.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/MiniSC_HC.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/ND.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/NDHC.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/ND_Compl_SC.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/ND_Compl_Truthtable.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/ND_Compl_Truthtable_Compact.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/ND_FiniteAssms.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/ND_Sound.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/Resolution.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/Resolution_Compl_Consistency.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/SC.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/SCND.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/SC_Depth.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/SC_Depth_Limit.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/SC_Sema.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/Substitution_Sema.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/Tseytin_Sema.thy` (diff)
The file was modified	`thys/Prpu_Maxflow/Fifo_Push_Relabel_Impl.thy` (diff)
The file was modified	`thys/Prpu_Maxflow/Generic_Push_Relabel.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/PseudoHoops/PseudoHoops.thy` (diff)
The file was modified	`thys/PseudoHoops/PseudoWaisbergAlgebra.thy` (diff)
The file was modified	`thys/PseudoHoops/RightComplementedMonoid.thy` (diff)
The file was modified	`thys/PseudoHoops/SpecialPseudoHoops.thy` (diff)
The file was modified	`thys/Psi_Calculi/Semantics.thy` (diff)
The file was modified	`thys/Ptolemys_Theorem/Ptolemys_Theorem.thy` (diff)
The file was modified	`thys/QR_Decomposition/Generalizations2.thy` (diff)
The file was modified	`thys/QR_Decomposition/Gram_Schmidt_IArrays.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/Quick_Sort_Cost/Randomised_Quick_Sort.thy` (diff)
The file was modified	`thys/ROBDD/BDD_Examples.thy` (diff)
The file was modified	`thys/ROBDD/Conc_Impl.thy` (diff)
The file was modified	`thys/ROBDD/Middle_Impl.thy` (diff)
The file was modified	`thys/RSAPSS/EMSAPSS.thy` (diff)
The file was modified	`thys/RSAPSS/WordOperations.thy` (diff)
The file was modified	`thys/Random_BSTs/Random_BSTs.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Automation/Preference_Profile_Cmd.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Automation/SDS_Automation.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Elections.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/SDS_Lowering.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Social_Decision_Schemes.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Dual_Order.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Fundamental_Subspaces.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/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_Graph.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/Snippets/Sepref_Snip_Combinator.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Examples/Snippets/Sepref_Snip_Datatype.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Examples/Worklist_Subsumption_Impl.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/Heaps/IICF_Impl_Heapmap.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_List_Mset.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/IICF_List_MsetO.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Impl/IICF_List_SetO.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Intf/IICF_List.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Intf/IICF_Map.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Intf/IICF_Matrix.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Intf/IICF_Multiset.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Intf/IICF_Prio_Bag.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Intf/IICF_Prio_Map.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/IICF/Intf/IICF_Set.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Lib/Pf_Add.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Lib/User_Smashing.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Combinator_Setup.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Foreach.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_HOL_Bindings.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_ICF_Bindings.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Monadify.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Userguides/Sepref_Guide_Quickstart.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Userguides/Sepref_Guide_Reference.thy` (diff)
The file was modified	`thys/Refine_Monadic/Generic/RefineG_Recursion.thy` (diff)
The file was modified	`thys/Refine_Monadic/Generic/RefineG_Transfer.thy` (diff)
The file was modified	`thys/Refine_Monadic/Generic/RefineG_While.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_Automation.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_Basic.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_Foreach.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/Refine_Pfun.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_While.thy` (diff)
The file was modified	`thys/Refine_Monadic/refine_mono_prover.ML` (diff)
The file was modified	`thys/Regex_Equivalence/Deriv_Autos.thy` (diff)
The file was modified	`thys/Regular-Sets/Regular_Set.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/Relation_Algebra/Relation_Algebra_RTC.thy` (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/Involutive_Residuated.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/Ribbon_Proofs/More_Finite_Map.thy` (diff)
The file was modified	`thys/Ribbon_Proofs/Ribbons_Graphical.thy` (diff)
The file was modified	`thys/Ribbon_Proofs/Ribbons_Graphical_Soundness.thy` (diff)
The file was modified	`thys/Ribbon_Proofs/Ribbons_Interfaces.thy` (diff)
The file was modified	`thys/Ribbon_Proofs/Ribbons_Stratified.thy` (diff)
The file was modified	`thys/Robbins-Conjecture/Robbins_Conjecture.thy` (diff)
The file was modified	`thys/Root_Balanced_Tree/Time_Monad.thy` (diff)
The file was modified	`thys/Routing/IpRoute_Parser.thy` (diff)
The file was modified	`thys/Routing/Linorder_Helper.thy` (diff)
The file was modified	`thys/Routing/ReversePathFiltering.thy` (diff)
The file was modified	`thys/Routing/Routing_Table.thy` (diff)
The file was modified	`thys/SATSolverVerification/CNF.thy` (diff)
The file was modified	`thys/SPARCv8/SparcModel_MMU/Sparc_Instruction.thy` (diff)
The file was modified	`thys/SPARCv8/SparcModel_MMU/Sparc_Properties.thy` (diff)
The file was modified	`thys/Secondary_Sylow/GroupAction.thy` (diff)
The file was modified	`thys/Secondary_Sylow/SubgroupConjugation.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Refinement.thy` (diff)
The file was modified	`thys/Separata/Separata.thy` (diff)
The file was modified	`thys/Separation_Algebra/Separation_Algebra.thy` (diff)
The file was modified	`thys/Separation_Algebra/ex/capDL/Abstract_Separation_D.thy` (diff)
The file was modified	`thys/Separation_Algebra/ex/capDL/Types_D.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Automation.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Tools/Syntax_Match.thy` (diff)
The file was modified	`thys/Shivers-CFA/CPSUtils.thy` (diff)
The file was modified	`thys/Show/Old_Datatype/Old_Show.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_generator.ML` (diff)
The file was modified	`thys/Show/Show.thy` (diff)
The file was modified	`thys/Simpl/DPC0Expressions.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/ProcParEx.thy` (diff)
The file was modified	`thys/Simpl/ex/ProcParExSP.thy` (diff)
The file was modified	`thys/Simpl/ex/Quicksort.thy` (diff)
The file was modified	`thys/Simpl/ex/VcgEx.thy` (diff)
The file was modified	`thys/Simpl/ex/VcgExSP.thy` (diff)
The file was modified	`thys/Simple_Firewall/Common/GroupF.thy` (diff)
The file was modified	`thys/Simple_Firewall/Common/IP_Addr_WordInterval_toString.thy` (diff)
The file was modified	`thys/Simple_Firewall/Common/IP_Partition_Preliminaries.thy` (diff)
The file was modified	`thys/Simple_Firewall/Common/List_Product_More.thy` (diff)
The file was modified	`thys/Simple_Firewall/Common/Option_Helpers.thy` (diff)
The file was modified	`thys/Simple_Firewall/Generic_SimpleFw.thy` (diff)
The file was modified	`thys/Simple_Firewall/Service_Matrix.thy` (diff)
The file was modified	`thys/Splay_Tree/Splay_Heap.thy` (diff)
The file was modified	`thys/Sqrt_Babylonian/Log_Impl.thy` (diff)
The file was modified	`thys/Sqrt_Babylonian/NthRoot_Impl.thy` (diff)
The file was modified	`thys/Stable_Matching/Dual_Lattice.thy` (diff)
The file was modified	`thys/Stern_Brocot/Cotree.thy` (diff)
The file was modified	`thys/Stern_Brocot/Cotree_Algebra.thy` (diff)
The file was modified	`thys/Stern_Brocot/Stern_Brocot_Tree.thy` (diff)
The file was modified	`thys/Stirling_Formula/Ln_Gamma_Asymptotics.thy` (diff)
The file was modified	`thys/Stream_Fusion_Code/Stream_Fusion_Examples.thy` (diff)
The file was modified	`thys/Stream_Fusion_Code/Stream_Fusion_List.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Sturm_Theorem.thy` (diff)
The file was modified	`thys/Stuttering_Equivalence/StutterEquivalence.thy` (diff)
The file was modified	`thys/Subresultants/Binary_Exponentiation.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/SuperCalc/well_founded_continued.thy` (diff)
The file was modified	`thys/TLA/Intensional.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/Hyperbolic_Tarski.thy` (diff)
The file was modified	`thys/Tarskis_Geometry/Projective.thy` (diff)
The file was modified	`thys/Timed_Automata/Approx_Beta.thy` (diff)
The file was modified	`thys/Timed_Automata/Closure.thy` (diff)
The file was modified	`thys/Timed_Automata/DBM.thy` (diff)
The file was modified	`thys/Timed_Automata/DBM_Basics.thy` (diff)
The file was modified	`thys/Timed_Automata/DBM_Normalization.thy` (diff)
The file was modified	`thys/Timed_Automata/DBM_Operations.thy` (diff)
The file was modified	`thys/Timed_Automata/DBM_Zone_Semantics.thy` (diff)
The file was modified	`thys/Timed_Automata/Floyd_Warshall.thy` (diff)
The file was modified	`thys/Timed_Automata/Misc.thy` (diff)
The file was modified	`thys/Timed_Automata/Normalized_Zone_Semantics.thy` (diff)
The file was modified	`thys/Timed_Automata/Paths_Cycles.thy` (diff)
The file was modified	`thys/Timed_Automata/Regions.thy` (diff)
The file was modified	`thys/Timed_Automata/Regions_Beta.thy` (diff)
The file was modified	`thys/Timed_Automata/Timed_Automata.thy` (diff)
The file was modified	`thys/Transition_Systems_and_Automata/Automata/DFA.thy` (diff)
The file was modified	`thys/Transition_Systems_and_Automata/Automata/NFA.thy` (diff)
The file was modified	`thys/Transition_Systems_and_Automata/Basic/Basic.thy` (diff)
The file was modified	`thys/Transition_Systems_and_Automata/Basic/Implement.thy` (diff)
The file was modified	`thys/Transition_Systems_and_Automata/Basic/Refine.thy` (diff)
The file was modified	`thys/Transition_Systems_and_Automata/Basic/Sequence.thy` (diff)
The file was modified	`thys/Transition_Systems_and_Automata/Basic/Sequence_LTL.thy` (diff)
The file was modified	`thys/Transition_Systems_and_Automata/Basic/Sequence_Zip.thy` (diff)
The file was modified	`thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System.thy` (diff)
The file was modified	`thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Construction.thy` (diff)
The file was modified	`thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Extra.thy` (diff)
The file was modified	`thys/Transition_Systems_and_Automata/Transition_Systems/Transition_System_Refine.thy` (diff)
The file was modified	`thys/Transitive-Closure-II/RTrancl.thy` (diff)
The file was modified	`thys/Tree-Automata/Ta.thy` (diff)
The file was modified	`thys/Tree_Decomposition/TreewidthCompleteGraph.thy` (diff)
The file was modified	`thys/Tree_Decomposition/TreewidthTree.thy` (diff)
The file was modified	`thys/Triangle/Angles.thy` (diff)
The file was modified	`thys/Trie/Trie.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Card_Bijections.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Card_Bijections_Direct.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way_Core.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way_Entry1.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way_Entry10.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way_Entry11.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way_Entry12.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way_Entry2.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way_Entry3.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way_Entry4.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way_Entry5.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way_Entry6.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way_Entry7.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way_Entry8.thy` (diff)
The file was modified	`thys/Twelvefold_Way/Twelvefold_Way_Entry9.thy` (diff)
The file was modified	`thys/UPF/Normalisation.thy` (diff)
The file was modified	`thys/UPF_Firewall/Examples/NAT-FW/NAT-FW.thy` (diff)
The file was modified	`thys/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallDatatype.thy` (diff)
The file was modified	`thys/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallInt.thy` (diff)
The file was modified	`thys/UPF_Firewall/Examples/Transformation/Transformation.thy` (diff)
The file was modified	`thys/UPF_Firewall/Examples/Transformation/Transformation01.thy` (diff)
The file was modified	`thys/UPF_Firewall/Examples/Transformation/Transformation02.thy` (diff)
The file was modified	`thys/UPF_Firewall/FWNormalisation/NormalisationGenericProofs.thy` (diff)
The file was modified	`thys/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy` (diff)
The file was modified	`thys/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy` (diff)
The file was modified	`thys/UPF_Firewall/NAT/NAT.thy` (diff)
The file was modified	`thys/UPF_Firewall/PacketFilter/PolicyCombinators.thy` (diff)
The file was modified	`thys/UPF_Firewall/PacketFilter/PortCombinators.thy` (diff)
The file was modified	`thys/UPF_Firewall/PacketFilter/ProtocolPortCombinators.thy` (diff)
The file was modified	`thys/UPF_Firewall/StatefulFW/FTP.thy` (diff)
The file was modified	`thys/UPF_Firewall/StatefulFW/FTP_WithPolicy.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Imperative.thy` (diff)
The file was modified	`thys/Verified-Prover/Prover.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/UniformTieBreaking.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Almost_Full.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Almost_Full_Relations.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Kruskal_Examples.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Well_Quasi_Orders.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Wqo_Instances.thy` (diff)
The file was modified	`thys/Winding_Number_Eval/Cauchy_Index_Theorem.thy` (diff)
The file was modified	`thys/Winding_Number_Eval/Missing_Algebraic.thy` (diff)
The file was modified	`thys/Winding_Number_Eval/Missing_Topology.thy` (diff)
The file was modified	`thys/Winding_Number_Eval/Missing_Transcendental.thy` (diff)
The file was modified	`thys/Winding_Number_Eval/Winding_Number_Eval.thy` (diff)
The file was modified	`thys/Winding_Number_Eval/Winding_Number_Eval_Examples.thy` (diff)
The file was modified	`thys/Word_Lib/Hex_Words.thy` (diff)
The file was modified	`thys/Word_Lib/Norm_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_Lib.thy` (diff)
The file was modified	`thys/WorkerWrapper/FixedPointTheorems.thy` (diff)
The file was modified	`thys/WorkerWrapper/Nats.thy` (diff)
The file was modified	`thys/WorkerWrapper/Nub.thy` (diff)
The file was modified	`thys/WorkerWrapper/UnboxedNats.thy` (diff)
The file was modified	`thys/XML/Xml.thy` (diff)
The file was modified	`thys/Zeta_Function/Zeta_Function.thy` (diff)
The file was modified	`thys/pGCL/Healthiness.thy` (diff)
The file was modified	`thys/pGCL/Tutorial/LoopExamples.thy` (diff)
The file was modified	`thys/pGCL/Tutorial/Primitives.thy` (diff)