Changes

Summary

merged
eliminated old 'def' command;

Changeset 8581:57534afa7b2d by wenzelm: merged
Changeset 8580:7feeab0671f8 by wenzelm: eliminated old 'def' command;
The file was modified	`thys/MFMC_Countable/Max_Flow_Min_Cut_Countable.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/WS1S.thy` (diff)
The file was modified	`thys/Minimal_SSA/Irreducible.thy` (diff)
The file was modified	`thys/Myhill-Nerode/Myhill_1.thy` (diff)
The file was modified	`thys/Native_Word/Word_Misc.thy` (diff)
The file was modified	`thys/No_FTL_observers/Axioms.thy` (diff)
The file was modified	`thys/No_FTL_observers/SpaceTime.thy` (diff)
The file was modified	`thys/No_FTL_observers/SpecRel.thy` (diff)
The file was modified	`thys/Nominal2/Nominal2_Base.thy` (diff)
The file was modified	`thys/NormByEval/NBE.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/AttractorInductive.thy` (diff)
The file was modified	`thys/Parity_Game/AttractorStrategy.thy` (diff)
The file was modified	`thys/Parity_Game/Graph_TheoryCompatibility.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/Strategy.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/Planarity_Certificates/Planarity/Digraph_Map_Impl.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Executable_Permutations.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Planar_Complete.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Planar_Subgraph.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Verification/Check_Non_Planarity_Verification.thy` (diff)
The file was modified	`thys/Planarity_Certificates/l4v/lib/OptionMonad.thy` (diff)
The file was modified	`thys/Pop_Refinement/Second_Example.thy` (diff)
The file was modified	`thys/Possibilistic_Noninterference/Concrete.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/Prime_Harmonic_Series/Squarefree_Nat.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Compositionality.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Language_Semantics.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Resumption_Based.thy` (diff)
The file was modified	`thys/Probabilistic_Noninterference/Trace_Based.thy` (diff)
The file was modified	`thys/Probabilistic_System_Zoo/Nonempty_Bounded_Set.thy` (diff)
The file was modified	`thys/Probabilistic_System_Zoo/Vardi_Counterexample.thy` (diff)
The file was modified	`thys/Promela/Promela.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/CNF_Formulas_Sema.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/Compactness.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/LSC_Resolution.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/MiniSC_Craig.thy` (diff)
The file was modified	`thys/Propositional_Proof_Systems/Sema_Craig.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.thy` (diff)
The file was modified	`thys/QR_Decomposition/QR_Decomposition.thy` (diff)
The file was modified	`thys/QR_Decomposition/QR_Efficient.thy` (diff)
The file was modified	`thys/RSAPSS/Word.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/Random_Serial_Dictatorship.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/SDS_Lowering.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/SD_Efficiency.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Stochastic_Dominance.thy` (diff)
The file was modified	`thys/Randomised_Social_Choice/Utility_Functions.thy` (diff)
The file was modified	`thys/Rank_Nullity_Theorem/Dim_Formula.thy` (diff)
The file was modified	`thys/Real_Impl/Prime_Product.thy` (diff)
The file was modified	`thys/Real_Impl/Real_Impl.thy` (diff)
The file was modified	`thys/Real_Impl/Real_Unique_Impl.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/PRecFinSet.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/PRecFun.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/PRecFun2.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/PRecList.thy` (diff)
The file was modified	`thys/Recursion-Theory-I/PRecUnGr.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_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_Misc.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_While.thy` (diff)
The file was modified	`thys/RefinementReactive/Reactive.thy` (diff)
The file was modified	`thys/Regular-Sets/pEquivalence_Checking.thy` (diff)
The file was modified	`thys/Rep_Fin_Groups/Rep_Fin_Groups.thy` (diff)
The file was modified	`thys/Ribbon_Proofs/Ribbons_Graphical_Soundness.thy` (diff)
The file was modified	`thys/SDS_Impossibility/SDS_Impossibility.thy` (diff)
The file was modified	`thys/SIFUM_Type_Systems/Compositionality.thy` (diff)
The file was modified	`thys/SIFUM_Type_Systems/LocallySoundModeUse.thy` (diff)
The file was modified	`thys/Secondary_Sylow/GroupAction.thy` (diff)
The file was modified	`thys/Secondary_Sylow/SndSylow.thy` (diff)
The file was modified	`thys/Secondary_Sylow/SubgroupConjugation.thy` (diff)
The file was modified	`thys/Simple_Firewall/SimpleFw_Semantics.thy` (diff)
The file was modified	`thys/Sort_Encodings/G.thy` (diff)
The file was modified	`thys/Sort_Encodings/M.thy` (diff)
The file was modified	`thys/Sort_Encodings/Mcalc2C.thy` (diff)
The file was modified	`thys/Sort_Encodings/Sig.thy` (diff)
The file was modified	`thys/Sort_Encodings/T.thy` (diff)
The file was modified	`thys/Sqrt_Babylonian/NthRoot_Impl.thy` (diff)
The file was modified	`thys/Sqrt_Babylonian/Sqrt_Babylonian.thy` (diff)
The file was modified	`thys/Sqrt_Babylonian/Sqrt_Babylonian_Auxiliary.thy` (diff)
The file was modified	`thys/Stern_Brocot/Stern_Brocot_Tree.thy` (diff)
The file was modified	`thys/Strong_Security/Language_Composition.thy` (diff)
The file was modified	`thys/Strong_Security/Parallel_Composition.thy` (diff)
The file was modified	`thys/Strong_Security/Strongly_Secure_Skip_Assign.thy` (diff)
The file was modified	`thys/Strong_Security/Up_To_Technique.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Lib/Misc_Polynomial.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Sturm_Theorem.thy` (diff)
The file was modified	`thys/Stuttering_Equivalence/PLTL.thy` (diff)
The file was modified	`thys/TortoiseHare/Basis.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/Tree_Decomposition/TreewidthTree.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Grid.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Triangular_Function.thy` (diff)
The file was modified	`thys/UpDown_Scheme/Up.thy` (diff)
The file was modified	`thys/WHATandWHERE_Security/Language_Composition.thy` (diff)
The file was modified	`thys/WHATandWHERE_Security/Parallel_Composition.thy` (diff)
The file was modified	`thys/WHATandWHERE_Security/WHATWHERE_Secure_Skip_Assign.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Higman_OI.thy` (diff)
The file was modified	`thys/Well_Quasi_Orders/Kruskal.thy` (diff)