Changes

Summary

standardized towards new-style formal comments: isabelle update_comments from Isabelle/f075640b8868;

Changeset 8763:4e9be8238696 by wenzelm: standardized towards new-style formal comments: isabelle update_comments from Isabelle/f075640b8868;
The file was modified	`thys/AODV/Global_Invariants.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_Global_Invariants.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_Global_Invariants.thy` (diff)
The file was modified	`thys/AODV/variants/e_all_abcd/E_Global_Invariants.thy` (diff)
The file was modified	`thys/AVL-Trees/AVL2.thy` (diff)
The file was modified	`thys/Abortable_Linearizable_Modules/Consensus.thy` (diff)
The file was modified	`thys/Abortable_Linearizable_Modules/Idempotence.thy` (diff)
The file was modified	`thys/Abortable_Linearizable_Modules/SLin.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_Form.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Ex_Inter.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/Print.thy` (diff)
The file was modified	`thys/AnselmGod/AnselmGod.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Applicative_Option.thy` (diff)
The file was modified	`thys/Applicative_Lifting/Tree_Relabelling.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/Lib/Refine_Util.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/BDD/NormalizeTotalProof.thy` (diff)
The file was modified	`thys/BDD/ShareReduceRepListProof.thy` (diff)
The file was modified	`thys/Bernoulli/Bernoulli_Zeta.thy` (diff)
The file was modified	`thys/BinarySearchTree/BinaryTree.thy` (diff)
The file was modified	`thys/BinarySearchTree/BinaryTree_Map.thy` (diff)
The file was modified	`thys/BinarySearchTree/BinaryTree_TacticStyle.thy` (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-Queues/Binomial_Queue.thy` (diff)
The file was modified	`thys/Binomial-Queues/PQ_Implementation.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/Buildings/Building.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/CAVA_Automata/Digraph.thy` (diff)
The file was modified	`thys/CAVA_Automata/Lasso.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/BoolProgs/BoolProgs.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/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/step/Step.thy` (diff)
The file was modified	`thys/CISC-Kernel/step/Step_configuration.thy` (diff)
The file was modified	`thys/CISC-Kernel/trace/Rushby-with-Control/CISK.thy` (diff)
The file was modified	`thys/CISC-Kernel/trace/Rushby-with-Control/ISK.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/CISC-Kernel/trace/Rushby-with-Control/SK.thy` (diff)
The file was modified	`thys/CISC-Kernel/trace/Rushby-with-Control/Separation_kernel_model.thy` (diff)
The file was modified	`thys/Case_Labeling/Examples/Hoare/Labeled_Hoare.thy` (diff)
The file was modified	`thys/Catalan_Numbers/Catalan_Auxiliary_Integral.thy` (diff)
The file was modified	`thys/Category/Yoneda.thy` (diff)
The file was modified	`thys/Cauchy/CauchysMeanTheorem.thy` (diff)
The file was modified	`thys/ClockSynchInst/ICAInstance.thy` (diff)
The file was modified	`thys/ClockSynchInst/LynchInstance.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/Lazy_LList.thy` (diff)
The file was modified	`thys/Coinductive/Lazy_TLList.thy` (diff)
The file was modified	`thys/Collections/Examples/ICF/Exploration.thy` (diff)
The file was modified	`thys/Collections/Examples/ICF/Exploration_DFS.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/GenCF/Impl/Impl_Array_Hash_Map.thy` (diff)
The file was modified	`thys/Collections/ICF/DatRef.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/Algos.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/SetGA.thy` (diff)
The file was modified	`thys/Collections/ICF/gen_algo/SetIndex.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/ArrayHashMap_Impl.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/Fifo.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/HashMap.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/HashMap_Impl.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/ListSetImpl_NotDist.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/ListSetImpl_Sorted.thy` (diff)
The file was modified	`thys/Collections/ICF/impl/Trie_Impl.thy` (diff)
The file was modified	`thys/Collections/ICF/spec/AnnotatedListSpec.thy` (diff)
The file was modified	`thys/Collections/ICF/spec/ListSpec.thy` (diff)
The file was modified	`thys/Collections/ICF/spec/MapSpec.thy` (diff)
The file was modified	`thys/Collections/ICF/spec/PrioSpec.thy` (diff)
The file was modified	`thys/Collections/ICF/spec/SetSpec.thy` (diff)
The file was modified	`thys/Collections/Lib/Diff_Array.thy` (diff)
The file was modified	`thys/Collections/Userguides/Refine_Monadic_Userguide.thy` (diff)
The file was modified	`thys/Completeness/Base.thy` (diff)
The file was modified	`thys/Completeness/Completeness.thy` (diff)
The file was modified	`thys/Completeness/Formula.thy` (diff)
The file was modified	`thys/Completeness/PermutationLemmas.thy` (diff)
The file was modified	`thys/Completeness/Sequents.thy` (diff)
The file was modified	`thys/Completeness/Tree.thy` (diff)
The file was modified	`thys/Complx/OG_Soundness.thy` (diff)
The file was modified	`thys/Complx/ex/Examples.thy` (diff)
The file was modified	`thys/Complx/ex/SumArr.thy` (diff)
The file was modified	`thys/ComponentDependencies/DataDependencies.thy` (diff)
The file was modified	`thys/ComponentDependencies/DataDependenciesCaseStudy.thy` (diff)
The file was modified	`thys/ComponentDependencies/DataDependenciesConcreteValues.thy` (diff)
The file was modified	`thys/ConcurrentGC/Model.thy` (diff)
The file was modified	`thys/ConcurrentIMP/CIMP_vcg.thy` (diff)
The file was modified	`thys/Consensus_Refined/Consensus_Types.thy` (diff)
The file was modified	`thys/Consensus_Refined/Infra.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_Vote.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/Observing_Quorums_Opt.thy` (diff)
The file was modified	`thys/Consensus_Refined/Quorums.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/Consensus_Refined/Voting/Ate_Defs.thy` (diff)
The file was modified	`thys/Consensus_Refined/Voting/Ate_Proofs.thy` (diff)
The file was modified	`thys/Containers/Collection_Order.thy` (diff)
The file was modified	`thys/Containers/Containers_Userguide.thy` (diff)
The file was modified	`thys/Containers/Lexicographic_Order.thy` (diff)
The file was modified	`thys/Containers/Set_Impl.thy` (diff)
The file was modified	`thys/CoreC++/ClassRel.thy` (diff)
The file was modified	`thys/CoreC++/Decl.thy` (diff)
The file was modified	`thys/CoreC++/Execute.thy` (diff)
The file was modified	`thys/CoreC++/Expr.thy` (diff)
The file was modified	`thys/CoreC++/Objects.thy` (diff)
The file was modified	`thys/CoreC++/Progress.thy` (diff)
The file was modified	`thys/CoreC++/SmallStep.thy` (diff)
The file was modified	`thys/CoreC++/State.thy` (diff)
The file was modified	`thys/CoreC++/SubObj.thy` (diff)
The file was modified	`thys/CoreC++/Type.thy` (diff)
The file was modified	`thys/CoreC++/Value.thy` (diff)
The file was modified	`thys/CoreC++/WellType.thy` (diff)
The file was modified	`thys/CryptHOL/Computational_Model.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/Generative_Probabilistic_Value.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/CryptoBasedCompositionalProperties/CompLocalSecrets.thy` (diff)
The file was modified	`thys/CryptoBasedCompositionalProperties/Secrecy.thy` (diff)
The file was modified	`thys/CryptoBasedCompositionalProperties/Secrecy_types.thy` (diff)
The file was modified	`thys/CryptoBasedCompositionalProperties/inout.thy` (diff)
The file was modified	`thys/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/Nested_DFS.thy` (diff)
The file was modified	`thys/DFS_Framework/Examples/Tarjan.thy` (diff)
The file was modified	`thys/DFS_Framework/Examples/Tarjan_LowLink.thy` (diff)
The file was modified	`thys/DFS_Framework/Impl/Data/Simple_Impl.thy` (diff)
The file was modified	`thys/DFS_Framework/Invars/DFS_Invars_Basic.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_Refine_Aux.thy` (diff)
The file was modified	`thys/DFS_Framework/Param_DFS.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/ChangeEnv.thy` (diff)
The file was modified	`thys/Decl_Sem_Fun_PL/DenotCompleteFSet.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/Deep_Learning/PP_MPoly.thy` (diff)
The file was modified	`thys/Deep_Learning/PP_Poly_Mapping.thy` (diff)
The file was modified	`thys/Dependent_SIFUM_Type_Systems/Compositionality.thy` (diff)
The file was modified	`thys/Dijkstra_Shortest_Path/Dijkstra.thy` (diff)
The file was modified	`thys/Diophantine_Eqns_Lin_Hom/Linear_Diophantine_Equations.thy` (diff)
The file was modified	`thys/Diophantine_Eqns_Lin_Hom/List_Vector.thy` (diff)
The file was modified	`thys/Diophantine_Eqns_Lin_Hom/Solver_Code.thy` (diff)
The file was modified	`thys/Dirichlet_L/Dirichlet_L_Functions.thy` (diff)
The file was modified	`thys/Dirichlet_Series/Dirichlet_Series_Analysis.thy` (diff)
The file was modified	`thys/Discrete_Summation/Factorials.thy` (diff)
The file was modified	`thys/DiskPaxos/DiskPaxos_Inv1.thy` (diff)
The file was modified	`thys/DiskPaxos/DiskPaxos_Inv4.thy` (diff)
The file was modified	`thys/DiskPaxos/DiskPaxos_Inv5.thy` (diff)
The file was modified	`thys/EdmondsKarp_Maxflow/Augmenting_Path_BFS.thy` (diff)
The file was modified	`thys/EdmondsKarp_Maxflow/EdmondsKarp_Algo.thy` (diff)
The file was modified	`thys/EdmondsKarp_Maxflow/EdmondsKarp_Impl.thy` (diff)
The file was modified	`thys/EdmondsKarp_Maxflow/EdmondsKarp_Termination_Abstract.thy` (diff)
The file was modified	`thys/EdmondsKarp_Maxflow/FordFulkerson_Algo.thy` (diff)
The file was modified	`thys/Example-Submission/Submission.thy` (diff)
The file was modified	`thys/FLP/Execution.thy` (diff)
The file was modified	`thys/FLP/FLPExistingSystem.thy` (diff)
The file was modified	`thys/FLP/FLPSystem.thy` (diff)
The file was modified	`thys/FLP/FLPTheorem.thy` (diff)
The file was modified	`thys/Fermat3_4/Fermat3.thy` (diff)
The file was modified	`thys/Fermat3_4/Fermat4.thy` (diff)
The file was modified	`thys/FileRefinement/FileRefinement.thy` (diff)
The file was modified	`thys/Finger-Trees/FingerTree.thy` (diff)
The file was modified	`thys/Flow_Networks/Augmenting_Flow.thy` (diff)
The file was modified	`thys/Flow_Networks/Augmenting_Path.thy` (diff)
The file was modified	`thys/Flow_Networks/Ford_Fulkerson.thy` (diff)
The file was modified	`thys/Flow_Networks/Graph.thy` (diff)
The file was modified	`thys/Flow_Networks/Graph_Impl.thy` (diff)
The file was modified	`thys/Flow_Networks/Lib/Fofu_Abs_Base.thy` (diff)
The file was modified	`thys/Flow_Networks/NetCheck.thy` (diff)
The file was modified	`thys/Flow_Networks/Network.thy` (diff)
The file was modified	`thys/Flow_Networks/Network_Impl.thy` (diff)
The file was modified	`thys/Flow_Networks/Residual_Graph.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/FR.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/stream.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/FunWithTilings/Tilings.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.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/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_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_UPF_IND_CCA.thy` (diff)
The file was modified	`thys/Game_Based_Crypto/SUF_CMA.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Elementary_Operations.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Gauss_Jordan.thy` (diff)
The file was modified	`thys/Gauss_Jordan/Inverse.thy` (diff)
The file was modified	`thys/Girth_Chromatic/Girth_Chromatic.thy` (diff)
The file was modified	`thys/GoedelGod/GoedelGod.thy` (diff)
The file was modified	`thys/Graph_Theory/Euler.thy` (diff)
The file was modified	`thys/HRB-Slicing/Proc/Com.thy` (diff)
The file was modified	`thys/Heard_Of/HOModel.thy` (diff)
The file was modified	`thys/Heard_Of/Reduction.thy` (diff)
The file was modified	`thys/Heard_Of/ate/AteDefs.thy` (diff)
The file was modified	`thys/Heard_Of/ate/AteProof.thy` (diff)
The file was modified	`thys/Heard_Of/eigbyz/EigbyzDefs.thy` (diff)
The file was modified	`thys/Heard_Of/eigbyz/EigbyzProof.thy` (diff)
The file was modified	`thys/Heard_Of/lastvoting/LastVotingDefs.thy` (diff)
The file was modified	`thys/Heard_Of/lastvoting/LastVotingProof.thy` (diff)
The file was modified	`thys/Heard_Of/otr/OneThirdRuleDefs.thy` (diff)
The file was modified	`thys/Heard_Of/otr/OneThirdRuleProof.thy` (diff)
The file was modified	`thys/Heard_Of/ute/UteDefs.thy` (diff)
The file was modified	`thys/Heard_Of/ute/UteProof.thy` (diff)
The file was modified	`thys/Heard_Of/uv/UvDefs.thy` (diff)
The file was modified	`thys/Heard_Of/uv/UvProof.thy` (diff)
The file was modified	`thys/HereditarilyFinite/HF.thy` (diff)
The file was modified	`thys/Huffman/Huffman.thy` (diff)
The file was modified	`thys/Hybrid_Multi_Lane_Spatial_Logic/HMLSL.thy` (diff)
The file was modified	`thys/IEEE_Floating_Point/Code_Float.thy` (diff)
The file was modified	`thys/IMAP-CRDT/IMAP-proof-helpers.thy` (diff)
The file was modified	`thys/IP_Addresses/IP_Address_toString.thy` (diff)
The file was modified	`thys/IP_Addresses/IPv4.thy` (diff)
The file was modified	`thys/IP_Addresses/IPv6.thy` (diff)
The file was modified	`thys/IP_Addresses/WordInterval.thy` (diff)
The file was modified	`thys/Imperative_Insertion_Sort/Imperative_Loops.thy` (diff)
The file was modified	`thys/Incompleteness/Coding.thy` (diff)
The file was modified	`thys/Incompleteness/Functions.thy` (diff)
The file was modified	`thys/Incompleteness/Goedel_I.thy` (diff)
The file was modified	`thys/Incompleteness/II_Prelims.thy` (diff)
The file was modified	`thys/Incompleteness/Predicates.thy` (diff)
The file was modified	`thys/Incompleteness/Quote.thy` (diff)
The file was modified	`thys/Incompleteness/Sigma.thy` (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/Inductive_Confidentiality/DolevYao/Event.thy` (diff)
The file was modified	`thys/Inductive_Confidentiality/DolevYao/Message.thy` (diff)
The file was modified	`thys/Inductive_Confidentiality/DolevYao/Public.thy` (diff)
The file was modified	`thys/Inductive_Confidentiality/GeneralAttacker/EventGA.thy` (diff)
The file was modified	`thys/Inductive_Confidentiality/GeneralAttacker/MessageGA.thy` (diff)
The file was modified	`thys/Inductive_Confidentiality/GeneralAttacker/PublicGA.thy` (diff)
The file was modified	`thys/Integration/MonConv.thy` (diff)
The file was modified	`thys/Integration/Sigma_Algebra.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Access_Matrix_Embeddings.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Call_Return_Unfolding.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Common/WordInterval_Lists.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Documentation.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Matching_Embeddings.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Common_Primitive_Matcher_Generic.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/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/No_Spoof.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Primitive_Matchers/Output_Interface_Replace.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/Ruleset_Update.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Embeddings.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Stateful.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Ternary/Matching_Ternary.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Ternary/Optimizing.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Semantics_Ternary/Primitive_Normalization.thy` (diff)
The file was modified	`thys/Iptables_Semantics/Simple_Firewall/SimpleFw_Compliance.thy` (diff)
The file was modified	`thys/Jinja/BV/BVExec.thy` (diff)
The file was modified	`thys/Jinja/BV/BVSpec.thy` (diff)
The file was modified	`thys/Jinja/BV/BVSpecTypeSafe.thy` (diff)
The file was modified	`thys/Jinja/BV/Effect.thy` (diff)
The file was modified	`thys/Jinja/BV/TF_JVM.thy` (diff)
The file was modified	`thys/Jinja/Common/Decl.thy` (diff)
The file was modified	`thys/Jinja/Common/Objects.thy` (diff)
The file was modified	`thys/Jinja/Common/Type.thy` (diff)
The file was modified	`thys/Jinja/Common/Value.thy` (diff)
The file was modified	`thys/Jinja/Compiler/Correctness2.thy` (diff)
The file was modified	`thys/Jinja/Compiler/J1WellForm.thy` (diff)
The file was modified	`thys/Jinja/DFA/Kildall.thy` (diff)
The file was modified	`thys/Jinja/J/Expr.thy` (diff)
The file was modified	`thys/Jinja/J/Progress.thy` (diff)
The file was modified	`thys/Jinja/J/SmallStep.thy` (diff)
The file was modified	`thys/Jinja/J/State.thy` (diff)
The file was modified	`thys/Jinja/J/TypeSafe.thy` (diff)
The file was modified	`thys/Jinja/J/WellType.thy` (diff)
The file was modified	`thys/Jinja/J/WellTypeRT.thy` (diff)
The file was modified	`thys/Jinja/JVM/JVMDefensive.thy` (diff)
The file was modified	`thys/Jinja/JVM/JVMExec.thy` (diff)
The file was modified	`thys/Jinja/JVM/JVMInstructions.thy` (diff)
The file was modified	`thys/Jinja/JVM/JVMState.thy` (diff)
The file was modified	`thys/JinjaThreads/BV/BVExec.thy` (diff)
The file was modified	`thys/JinjaThreads/BV/BVSpec.thy` (diff)
The file was modified	`thys/JinjaThreads/BV/TF_JVM.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/BinOp.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/Decl.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/ExternalCall.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/Heap.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/Type.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/TypeRel.thy` (diff)
The file was modified	`thys/JinjaThreads/Common/Value.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/Compiler2.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J0.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J1JVMBisim.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J1State.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/J1WellType.thy` (diff)
The file was modified	`thys/JinjaThreads/Compiler/JVMTau.thy` (diff)
The file was modified	`thys/JinjaThreads/DFA/Kildall.thy` (diff)
The file was modified	`thys/JinjaThreads/Execute/Round_Robin.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWDeadlock.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/FWLTS.thy` (diff)
The file was modified	`thys/JinjaThreads/J/Annotate.thy` (diff)
The file was modified	`thys/JinjaThreads/J/Expr.thy` (diff)
The file was modified	`thys/JinjaThreads/J/Progress.thy` (diff)
The file was modified	`thys/JinjaThreads/J/SmallStep.thy` (diff)
The file was modified	`thys/JinjaThreads/J/State.thy` (diff)
The file was modified	`thys/JinjaThreads/J/Threaded.thy` (diff)
The file was modified	`thys/JinjaThreads/J/TypeSafe.thy` (diff)
The file was modified	`thys/JinjaThreads/J/WellType.thy` (diff)
The file was modified	`thys/JinjaThreads/JVM/JVMInstructions.thy` (diff)
The file was modified	`thys/JinjaThreads/JVM/JVMState.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/JMM_Typesafe.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/SC.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/SC_Collections.thy` (diff)
The file was modified	`thys/JiveDataStoreModel/Isa_Counter/TypeIds.thy` (diff)
The file was modified	`thys/JiveDataStoreModel/Isabelle/Subtype.thy` (diff)
The file was modified	`thys/JiveDataStoreModel/Isabelle/Value.thy` (diff)
The file was modified	`thys/JiveDataStoreModel/Isabelle_Store/AttributesIndep.thy` (diff)
The file was modified	`thys/JiveDataStoreModel/Isabelle_Store/Location.thy` (diff)
The file was modified	`thys/JiveDataStoreModel/Isabelle_Store/Store.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/KBPs/KBPsAlg.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Dioid_Models.thy` (diff)
The file was modified	`thys/Kleene_Algebra/Formal_Power_Series.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/Knuth_Morris_Pratt/KMP.thy` (diff)
The file was modified	`thys/LTL/LTL.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/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/LTL_Rabin_Impl.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Impl/Mojmir_Rabin_Impl.thy` (diff)
The file was modified	`thys/LTL_to_DRA/LTL_FGXU.thy` (diff)
The file was modified	`thys/LTL_to_DRA/LTL_Rabin.thy` (diff)
The file was modified	`thys/LTL_to_DRA/LTL_Rabin_Unfold_Opt.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Mojmir.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Semi_Mojmir.thy` (diff)
The file was modified	`thys/LTL_to_DRA/af.thy` (diff)
The file was modified	`thys/LTL_to_GBA/LTL_Stutter.thy` (diff)
The file was modified	`thys/Lam-ml-Normalization/Lam_ml.thy` (diff)
The file was modified	`thys/Latin_Square/Latin_Square.thy` (diff)
The file was modified	`thys/Launchbury/ResourcedAdequacy.thy` (diff)
The file was modified	`thys/LightweightJava/Lightweight_Java_Proof.thy` (diff)
The file was modified	`thys/Liouville_Numbers/Liouville_Numbers.thy` (diff)
The file was modified	`thys/List_Update/BIT.thy` (diff)
The file was modified	`thys/List_Update/TS.thy` (diff)
The file was modified	`thys/Locally-Nameless-Sigma/Sigma/Sigma.thy` (diff)
The file was modified	`thys/Lowe_Ontological_Argument/LoweOntologicalArgument_1.thy` (diff)
The file was modified	`thys/Lowe_Ontological_Argument/LoweOntologicalArgument_2.thy` (diff)
The file was modified	`thys/Lowe_Ontological_Argument/LoweOntologicalArgument_3.thy` (diff)
The file was modified	`thys/Lowe_Ontological_Argument/LoweOntologicalArgument_6.thy` (diff)
The file was modified	`thys/Lowe_Ontological_Argument/LoweOntologicalArgument_7.thy` (diff)
The file was modified	`thys/Lowe_Ontological_Argument/QML.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/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/ex/MDP_RP_Certification.thy` (diff)
The file was modified	`thys/Marriage/Marriage.thy` (diff)
The file was modified	`thys/Median_Of_Medians_Selection/Median_Of_Medians_Selection.thy` (diff)
The file was modified	`thys/Menger/DisjointPaths.thy` (diff)
The file was modified	`thys/Menger/Graph.thy` (diff)
The file was modified	`thys/Menger/MengerInduction.thy` (diff)
The file was modified	`thys/Menger/Y_eq_new_last.thy` (diff)
The file was modified	`thys/Menger/Y_neq_new_last.thy` (diff)
The file was modified	`thys/MiniML/Generalize.thy` (diff)
The file was modified	`thys/MiniML/Maybe.thy` (diff)
The file was modified	`thys/MiniML/MiniML.thy` (diff)
The file was modified	`thys/MiniML/Type.thy` (diff)
The file was modified	`thys/MiniML/W.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/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/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_Bisimilarity_Implies_Equivalence.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/Weak_Equivalence_Implies_Bisimilarity.thy` (diff)
The file was modified	`thys/Modal_Logics_for_NTS/Weak_Transition_System.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/Nat-Interval-Logic/IL_TemporalOperators.thy` (diff)
The file was modified	`thys/Native_Word/Bits_Integer.thy` (diff)
The file was modified	`thys/Native_Word/Native_Word_Test.thy` (diff)
The file was modified	`thys/Native_Word/Native_Word_Test_Emu.thy` (diff)
The file was modified	`thys/Native_Word/Uint.thy` (diff)
The file was modified	`thys/Native_Word/Uint_Userguide.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Distributed_WebApp.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Examples/Example_NetModel.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Lib/FiniteGraph.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/Lib/FiniteListGraph.thy` (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/Security_Invariants/SINVAR_NonInterference.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Composition_Theory.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Composition_Theory_impl.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_ENF.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Interface.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Interface_impl.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Stateful_Policy.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Stateful_Policy_Algorithm.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Stateful_Policy_impl.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_Vertices.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_generateCode.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/TopoS_withOffendingFlows.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/attic.thy` (diff)
The file was modified	`thys/Network_Security_Policy_Verification/vertex_example_simps.thy` (diff)
The file was modified	`thys/NormByEval/NBE.thy` (diff)
The file was modified	`thys/Optics/Interp.thy` (diff)
The file was modified	`thys/Orbit_Stabiliser/Left_Coset.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_C1.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/Reachability_Analysis.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/Matrix_Exponential.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/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/PCF/SmallStep.thy` (diff)
The file was modified	`thys/PLM/TAO_1_Embedding.thy` (diff)
The file was modified	`thys/PLM/TAO_7_Axioms.thy` (diff)
The file was modified	`thys/PLM/TAO_98_ArtificialTheorems.thy` (diff)
The file was modified	`thys/PLM/TAO_99_SanityTests.thy` (diff)
The file was modified	`thys/PLM/TAO_9_PLM.thy` (diff)
The file was modified	`thys/POPLmark-deBruijn/POPLmark.thy` (diff)
The file was modified	`thys/POPLmark-deBruijn/POPLmarkRecord.thy` (diff)
The file was modified	`thys/POPLmark-deBruijn/POPLmarkRecordCtxt.thy` (diff)
The file was modified	`thys/Parity_Game/AttractingStrategy.thy` (diff)
The file was modified	`thys/Parity_Game/Attractor.thy` (diff)
The file was modified	`thys/Parity_Game/AttractorStrategy.thy` (diff)
The file was modified	`thys/Parity_Game/ParityGame.thy` (diff)
The file was modified	`thys/Parity_Game/PositionalDeterminacy.thy` (diff)
The file was modified	`thys/Parity_Game/UniformStrategy.thy` (diff)
The file was modified	`thys/Parity_Game/WellOrderedStrategy.thy` (diff)
The file was modified	`thys/Parity_Game/WinningRegion.thy` (diff)
The file was modified	`thys/Parity_Game/WinningStrategy.thy` (diff)
The file was modified	`thys/Pop_Refinement/First_Example.thy` (diff)
The file was modified	`thys/Pop_Refinement/Second_Example.thy` (diff)
The file was modified	`thys/Prime_Harmonic_Series/Prime_Harmonic.thy` (diff)
The file was modified	`thys/Probabilistic_System_Zoo/Finitely_Bounded_Set_Counterexample.thy` (diff)
The file was modified	`thys/Probabilistic_System_Zoo/Vardi_Counterexample.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/ConstraintSystems.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Flowgraph.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/Interleave.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/LTS.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/MainResult.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/Program-Conflict-Analysis/Semantics.thy` (diff)
The file was modified	`thys/Program-Conflict-Analysis/ThreadTracking.thy` (diff)
The file was modified	`thys/Promela/Promela.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/Propositional_Proof_Systems/Consistency.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/Formulas.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/LSC.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/SC_Sema.thy` (diff)
The file was modified	`thys/Prpu_Maxflow/Fifo_Push_Relabel.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/Prpu_Maxflow/Prpu_Common_Impl.thy` (diff)
The file was modified	`thys/Prpu_Maxflow/Relabel_To_Front.thy` (diff)
The file was modified	`thys/Prpu_Maxflow/Relabel_To_Front_Impl.thy` (diff)
The file was modified	`thys/QR_Decomposition/Gram_Schmidt_IArrays.thy` (diff)
The file was modified	`thys/Ramsey-Infinite/Ramsey.thy` (diff)
The file was modified	`thys/Random_Graph_Subgraph_Threshold/Prob_Lemmas.thy` (diff)
The file was modified	`thys/Random_Graph_Subgraph_Threshold/Subgraph_Threshold.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/Rank_Nullity_Theorem/Dim_Formula.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/RecEnSet.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Examples/Sepref_DFS.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.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_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/Lib/Term_Synth.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Basic.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Frame.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_HOL_Bindings.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Id_Op.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Monadify.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Rules.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Sepref_Translate.thy` (diff)
The file was modified	`thys/Refine_Imperative_HOL/Userguides/Sepref_Guide_General_Util.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_Domain.thy` (diff)
The file was modified	`thys/Refine_Monadic/Generic/RefineG_Recursion.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_Basic.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_Det.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_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_While.thy` (diff)
The file was modified	`thys/Refine_Monadic/examples/Breadth_First_Search.thy` (diff)
The file was modified	`thys/Refine_Monadic/examples/WordRefine.thy` (diff)
The file was modified	`thys/Regular_Algebras/Regular_Algebra_Variants.thy` (diff)
The file was modified	`thys/Regular_Algebras/Regular_Algebras.thy` (diff)
The file was modified	`thys/Rep_Fin_Groups/Rep_Fin_Groups.thy` (diff)
The file was modified	`thys/Resolution_FOL/Completeness.thy` (diff)
The file was modified	`thys/Resolution_FOL/Resolution.thy` (diff)
The file was modified	`thys/Resolution_FOL/TermsAndLiterals.thy` (diff)
The file was modified	`thys/Ribbon_Proofs/Ribbons_Interfaces.thy` (diff)
The file was modified	`thys/SATSolverVerification/SatSolverCode.thy` (diff)
The file was modified	`thys/SIFUM_Type_Systems/Compositionality.thy` (diff)
The file was modified	`thys/SPARCv8/SparcModel_MMU/Sparc_Types.thy` (diff)
The file was modified	`thys/Secondary_Sylow/SndSylow.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Keys.thy` (diff)
The file was modified	`thys/Security_Protocol_Refinement/Refinement/Message.thy` (diff)
The file was modified	`thys/Selection_Heap_Sort/Heap.thy` (diff)
The file was modified	`thys/Selection_Heap_Sort/RemoveMax.thy` (diff)
The file was modified	`thys/SenSocialChoice/Arrow.thy` (diff)
The file was modified	`thys/SenSocialChoice/May.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/Hoare_Triple.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Run.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/SingleSuccedent.thy` (diff)
The file was modified	`thys/Show/Show.thy` (diff)
The file was modified	`thys/Simpl/HoarePartial.thy` (diff)
The file was modified	`thys/Simpl/HoareTotal.thy` (diff)
The file was modified	`thys/Simple_Firewall/Generic_SimpleFw.thy` (diff)
The file was modified	`thys/Simple_Firewall/Primitives/Iface.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/Slicing/Dynamic/DynPDG.thy` (diff)
The file was modified	`thys/Slicing/While/Com.thy` (diff)
The file was modified	`thys/Sort_Encodings/Encodings.thy` (diff)
The file was modified	`thys/Special_Function_Bounds/Exp_Bounds.thy` (diff)
The file was modified	`thys/Special_Function_Bounds/Sin_Cos_Bounds.thy` (diff)
The file was modified	`thys/Stable_Matching/COP.thy` (diff)
The file was modified	`thys/Stable_Matching/Choice_Functions.thy` (diff)
The file was modified	`thys/Stable_Matching/Sotomayor.thy` (diff)
The file was modified	`thys/Stable_Matching/Strategic.thy` (diff)
The file was modified	`thys/Stern_Brocot/Bird_Tree.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/Strong_Security/Domain_example.thy` (diff)
The file was modified	`thys/Strong_Security/Expr.thy` (diff)
The file was modified	`thys/Strong_Security/Language_Composition.thy` (diff)
The file was modified	`thys/Strong_Security/MWLf.thy` (diff)
The file was modified	`thys/Strong_Security/Strong_Security.thy` (diff)
The file was modified	`thys/Strong_Security/Strongly_Secure_Skip_Assign.thy` (diff)
The file was modified	`thys/Strong_Security/Type_System.thy` (diff)
The file was modified	`thys/Strong_Security/Type_System_example.thy` (diff)
The file was modified	`thys/Strong_Security/Types.thy` (diff)
The file was modified	`thys/Strong_Security/Up_To_Technique.thy` (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/SumSquares/FourSquares.thy` (diff)
The file was modified	`thys/SumSquares/TwoSquares.thy` (diff)
The file was modified	`thys/TLA/Buffer.thy` (diff)
The file was modified	`thys/TLA/Rules.thy` (diff)
The file was modified	`thys/TLA/Semantics.thy` (diff)
The file was modified	`thys/TLA/Sequence.thy` (diff)
The file was modified	`thys/TLA/State.thy` (diff)
The file was modified	`thys/Taylor_Models/Interval.thy` (diff)
The file was modified	`thys/Taylor_Models/Polynomial_Expression.thy` (diff)
The file was modified	`thys/Taylor_Models/Polynomial_Expression_Additional.thy` (diff)
The file was modified	`thys/Taylor_Models/Taylor_Models.thy` (diff)
The file was modified	`thys/Timed_Automata/Misc.thy` (diff)
The file was modified	`thys/Topology/Topology.thy` (diff)
The file was modified	`thys/TortoiseHare/Brent.thy` (diff)
The file was modified	`thys/TortoiseHare/TortoiseHare.thy` (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/Tree_Decomposition/Graph.thy` (diff)
The file was modified	`thys/Tree_Decomposition/Tree.thy` (diff)
The file was modified	`thys/Tree_Decomposition/TreeDecomposition.thy` (diff)
The file was modified	`thys/Types_Tableaus_and_Goedels_God/AndersonProof.thy` (diff)
The file was modified	`thys/Types_Tableaus_and_Goedels_God/FittingProof.thy` (diff)
The file was modified	`thys/Types_Tableaus_and_Goedels_God/GoedelProof_P1.thy` (diff)
The file was modified	`thys/Types_Tableaus_and_Goedels_God/GoedelProof_P2.thy` (diff)
The file was modified	`thys/Types_Tableaus_and_Goedels_God/IHOML.thy` (diff)
The file was modified	`thys/Types_Tableaus_and_Goedels_God/IHOML_Examples.thy` (diff)
The file was modified	`thys/VectorSpace/VectorSpace.thy` (diff)
The file was modified	`thys/Verified-Prover/Prover.thy` (diff)
The file was modified	`thys/VolpanoSmith/Semantics.thy` (diff)
The file was modified	`thys/VolpanoSmith/secTypes.thy` (diff)
The file was modified	`thys/WHATandWHERE_Security/Language_Composition.thy` (diff)
The file was modified	`thys/WHATandWHERE_Security/MWLs.thy` (diff)
The file was modified	`thys/WHATandWHERE_Security/Parallel_Composition.thy` (diff)
The file was modified	`thys/WHATandWHERE_Security/Type_System.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_Secure_Skip_Assign.thy` (diff)
The file was modified	`thys/WHATandWHERE_Security/WHATWHERE_Security.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Higman_OI.thy` (diff)
The file was modified	`thys/WorkerWrapper/FixedPointTheorems.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/LoopInduction.thy` (diff)
The file was modified	`thys/pGCL/Termination.thy` (diff)
The file was modified	`thys/pGCL/Tutorial/Monty.thy` (diff)