Changes

Summary

updated to Isabelle/056ea294c256;
eliminated use of empty "assms";

Changeset 6606:55c683570c16 by wenzelm: updated to Isabelle/056ea294c256;
The file was modified	`thys/Featherweight_OCL/src/UML_Types.thy` (diff)
The file was modified	`thys/Isabelle_Meta_Model/toy_example/embedding/Generator_dynamic.thy` (diff)
Changeset 6605:96c7d6e86e89 by wenzelm: eliminated use of empty "assms";
The file was modified	`thys/AODV/Aodv.thy` (diff)
The file was modified	`thys/AODV/Aodv_Data.thy` (diff)
The file was modified	`thys/AODV/Fresher.thy` (diff)
The file was modified	`thys/AODV/variants/a_norreqid/A_Aodv.thy` (diff)
The file was modified	`thys/AODV/variants/a_norreqid/A_Aodv_Data.thy` (diff)
The file was modified	`thys/AODV/variants/a_norreqid/A_Fresher.thy` (diff)
The file was modified	`thys/AODV/variants/b_fwdrreps/B_Aodv.thy` (diff)
The file was modified	`thys/AODV/variants/b_fwdrreps/B_Aodv_Data.thy` (diff)
The file was modified	`thys/AODV/variants/b_fwdrreps/B_Fresher.thy` (diff)
The file was modified	`thys/AODV/variants/c_gtobcast/C_Aodv.thy` (diff)
The file was modified	`thys/AODV/variants/c_gtobcast/C_Aodv_Data.thy` (diff)
The file was modified	`thys/AODV/variants/c_gtobcast/C_Fresher.thy` (diff)
The file was modified	`thys/AODV/variants/d_fwdrreqs/D_Aodv.thy` (diff)
The file was modified	`thys/AODV/variants/d_fwdrreqs/D_Aodv_Data.thy` (diff)
The file was modified	`thys/AODV/variants/d_fwdrreqs/D_Fresher.thy` (diff)
The file was modified	`thys/AODV/variants/e_all_abcd/E_Aodv.thy` (diff)
The file was modified	`thys/AODV/variants/e_all_abcd/E_Aodv_Data.thy` (diff)
The file was modified	`thys/AODV/variants/e_all_abcd/E_Fresher.thy` (diff)
The file was modified	`thys/AVL-Trees/AVL.thy` (diff)
The file was modified	`thys/AWN/AWN.thy` (diff)
The file was modified	`thys/AWN/AWN_Cterms.thy` (diff)
The file was modified	`thys/AWN/OClosed_Transfer.thy` (diff)
The file was modified	`thys/AWN/Qmsg.thy` (diff)
The file was modified	`thys/AWN/Toy.thy` (diff)
The file was modified	`thys/Abortable_Linearizable_Modules/Idempotence.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_Form.thy` (diff)
The file was modified	`thys/Affine_Arithmetic/Intersection.thy` (diff)
The file was modified	`thys/Akra_Bazzi/Master_Theorem.thy` (diff)
The file was modified	`thys/Bondy/Bondy.thy` (diff)
The file was modified	`thys/CAVA_Automata/Lasso.thy` (diff)
The file was modified	`thys/CAVA_LTL_Modelchecker/CAVA_Impl.thy` (diff)
The file was modified	`thys/CISC-Kernel/step/Step_invariants.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/Option_Binders.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/Call_Arity/SestoftGC.thy` (diff)
The file was modified	`thys/Coinductive/Coinductive_Nat.thy` (diff)
The file was modified	`thys/Coinductive/Examples/LList_CCPO_Topology.thy` (diff)
The file was modified	`thys/Collections/GenCF/Impl/Impl_List_Map.thy` (diff)
The file was modified	`thys/ConcurrentGC/Handshakes.thy` (diff)
The file was modified	`thys/ConcurrentGC/MarkObject.thy` (diff)
The file was modified	`thys/ConcurrentIMP/CIMP_unbounded_buffer_ex.thy` (diff)
The file was modified	`thys/Decreasing-Diagrams/Decreasing_Diagrams.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Density_Contexts.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Semantics.thy` (diff)
The file was modified	`thys/Density_Compiler/PDF_Values.thy` (diff)
The file was modified	`thys/Descartes_Sign_Rule/Descartes_Sign_Rule.thy` (diff)
The file was modified	`thys/DiskPaxos/DiskPaxos_Inv6.thy` (diff)
The file was modified	`thys/Ergodic_Theory/Recurrence.thy` (diff)
The file was modified	`thys/Ergodic_Theory/SG_Library_Complement.thy` (diff)
The file was modified	`thys/Finger-Trees/FingerTree.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/arith_hints.thy` (diff)
The file was modified	`thys/FocusStreamsCaseStudies/stream.thy` (diff)
The file was modified	`thys/Formal_SSA/Construct_SSA_code.thy` (diff)
The file was modified	`thys/Girth_Chromatic/Ugraphs.thy` (diff)
The file was modified	`thys/Graph_Theory/Bidirected_Digraph.thy` (diff)
The file was modified	`thys/Graph_Theory/Digraph_Component.thy` (diff)
The file was modified	`thys/Graph_Theory/Vertex_Walk.thy` (diff)
The file was modified	`thys/Groebner_Bases/Abstract_Poly.thy` (diff)
The file was modified	`thys/Groebner_Bases/Power_Products.thy` (diff)
The file was modified	`thys/HereditarilyFinite/Rank.thy` (diff)
The file was modified	`thys/HyperCTL/Deep.thy` (diff)
The file was modified	`thys/HyperCTL/Noninterference.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/SyntaxN.thy` (diff)
The file was modified	`thys/JinjaThreads/Basic/Auxiliary.thy` (diff)
The file was modified	`thys/JinjaThreads/Framework/LTS.thy` (diff)
The file was modified	`thys/JinjaThreads/MM/SC_Completion.thy` (diff)
The file was modified	`thys/Jordan_Hoelder/CompositionSeries.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Jordan_Normal_Form_Existence.thy` (diff)
The file was modified	`thys/Jordan_Normal_Form/Matrix.thy` (diff)
The file was modified	`thys/KBPs/List_local.thy` (diff)
The file was modified	`thys/Knot_Theory/Preliminaries.thy` (diff)
The file was modified	`thys/Knot_Theory/Tangles.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Logical_Characterization.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Mojmir_Rabin.thy` (diff)
The file was modified	`thys/LTL_to_DRA/Semi_Mojmir.thy` (diff)
The file was modified	`thys/LTL_to_GBA/LTL_to_GBA.thy` (diff)
The file was modified	`thys/Landau_Symbols/Group_Sort.thy` (diff)
The file was modified	`thys/Landau_Symbols/Landau_Library.thy` (diff)
The file was modified	`thys/Landau_Symbols/Landau_Real_Products.thy` (diff)
The file was modified	`thys/Landau_Symbols/Landau_Symbols_Definition.thy` (diff)
The file was modified	`thys/Latin_Square/Latin_Square.thy` (diff)
The file was modified	`thys/Launchbury/C-restr.thy` (diff)
The file was modified	`thys/Launchbury/Env-HOLCF.thy` (diff)
The file was modified	`thys/Lower_Semicontinuous/Lower_Semicontinuous.thy` (diff)
The file was modified	`thys/MSO_Regex_Equivalence/Pi_Regular_Set.thy` (diff)
The file was modified	`thys/Markov_Models/Discrete_Time_Markov_Chain.thy` (diff)
The file was modified	`thys/Markov_Models/ex/Crowds_Protocol.thy` (diff)
The file was modified	`thys/Matrix/Matrix_Arith.thy` (diff)
The file was modified	`thys/Matrix_Tensor/Matrix_Tensor.thy` (diff)
The file was modified	`thys/Nominal2/Nominal2_Abs.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/Numerics/Euler_Affine.thy` (diff)
The file was modified	`thys/Ordinary_Differential_Equations/Numerics/One_Step_Method.thy` (diff)
The file was modified	`thys/Parity_Game/MoreCoinductiveList.thy` (diff)
The file was modified	`thys/Parity_Game/ParityGame.thy` (diff)
The file was modified	`thys/Parity_Game/WellOrderedStrategy.thy` (diff)
The file was modified	`thys/Pi_Calculus/Weak_Early_Semantics.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Digraph_Map_Impl.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Graph_Genus.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Permutations_2.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Planar_Subdivision.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Planarity/Planar_Subgraph.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Verification/Check_Planarity_Verification.thy` (diff)
The file was modified	`thys/Planarity_Certificates/Verification/Setup_AutoCorres.thy` (diff)
The file was modified	`thys/Polynomial_Interpolation/Missing_Polynomial.thy` (diff)
The file was modified	`thys/Polynomials/Polynomials.thy` (diff)
The file was modified	`thys/Possibilistic_Noninterference/Compositionality.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/PropResPI/Prime_Implicates.thy` (diff)
The file was modified	`thys/PropResPI/Propositional_Resolution.thy` (diff)
The file was modified	`thys/Psi_Calculi/Agent.thy` (diff)
The file was modified	`thys/Psi_Calculi/Bisimulation.thy` (diff)
The file was modified	`thys/Psi_Calculi/Chain.thy` (diff)
The file was modified	`thys/Psi_Calculi/Semantics.thy` (diff)
The file was modified	`thys/Psi_Calculi/Sim_Struct_Cong.thy` (diff)
The file was modified	`thys/Psi_Calculi/Subst_Term.thy` (diff)
The file was modified	`thys/Psi_Calculi/Tau.thy` (diff)
The file was modified	`thys/Psi_Calculi/Tau_Laws_No_Weak.thy` (diff)
The file was modified	`thys/Psi_Calculi/Weak_Bisimulation.thy` (diff)
The file was modified	`thys/ROBDD/Level_Collapse.thy` (diff)
The file was modified	`thys/Refine_Monadic/Generic/RefineG_While.thy` (diff)
The file was modified	`thys/Refine_Monadic/Refine_Foreach.thy` (diff)
The file was modified	`thys/Regular-Sets/Regular_Set.thy` (diff)
The file was modified	`thys/Rep_Fin_Groups/Rep_Fin_Groups.thy` (diff)
The file was modified	`thys/Ribbon_Proofs/Ribbons_Graphical.thy` (diff)
The file was modified	`thys/SATSolverVerification/FunctionalImplementation.thy` (diff)
The file was modified	`thys/SATSolverVerification/Initialization.thy` (diff)
The file was modified	`thys/SATSolverVerification/MoreList.thy` (diff)
The file was modified	`thys/SATSolverVerification/Trail.thy` (diff)
The file was modified	`thys/Selection_Heap_Sort/SelectionSort_Functional.thy` (diff)
The file was modified	`thys/Separation_Logic_Imperative_HOL/Assertions.thy` (diff)
The file was modified	`thys/Shivers-CFA/CPSUtils.thy` (diff)
The file was modified	`thys/Sort_Encodings/G.thy` (diff)
The file was modified	`thys/Sort_Encodings/Mono.thy` (diff)
The file was modified	`thys/Sort_Encodings/Preliminaries.thy` (diff)
The file was modified	`thys/Sort_Encodings/T.thy` (diff)
The file was modified	`thys/Special_Function_Bounds/Atan_CF_Bounds.thy` (diff)
The file was modified	`thys/Special_Function_Bounds/Sqrt_Bounds.thy` (diff)
The file was modified	`thys/Sturm_Sequences/Sturm_Method.thy` (diff)
The file was modified	`thys/Timed_Automata/Approx_Beta.thy` (diff)
The file was modified	`thys/Timed_Automata/Normalized_Zone_Semantics.thy` (diff)
The file was modified	`thys/Timed_Automata/Regions_Beta.thy` (diff)
The file was modified	`thys/TortoiseHare/Basis.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/Argmax.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/CombinatorialAuction.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/MiscTools.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/RelationProperties.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/UniformTieBreaking.thy` (diff)
The file was modified	`thys/Vickrey_Clarke_Groves/Universes.thy` (diff)