Changes

Summary

removed legacy input syntax
added and tuned lemmas

Changeset 69313:b021008c5397 by haftmann: removed legacy input syntax
The file was modified	`src/Doc/Main/Main_Doc.thy` (diff)
The file was modified	`src/HOL/Algebra/FiniteProduct.thy` (diff)
The file was modified	`src/HOL/Analysis/Abstract_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Arcwise_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Binary_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Brouwer_Fixpoint.thy` (diff)
The file was modified	`src/HOL/Analysis/Caratheodory.thy` (diff)
The file was modified	`src/HOL/Analysis/Change_Of_Vars.thy` (diff)
The file was modified	`src/HOL/Analysis/Complete_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Embed_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Extended_Real_Limits.thy` (diff)
The file was modified	`src/HOL/Analysis/Finite_Product_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Henstock_Kurzweil_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Homeomorphism.thy` (diff)
The file was modified	`src/HOL/Analysis/Improper_Integral.thy` (diff)
The file was modified	`src/HOL/Analysis/Measure_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Path_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Polytope.thy` (diff)
The file was modified	`src/HOL/Analysis/Set_Integral.thy` (diff)
The file was modified	`src/HOL/Analysis/Sigma_Algebra.thy` (diff)
The file was modified	`src/HOL/Analysis/Starlike.thy` (diff)
The file was modified	`src/HOL/Analysis/Topology_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Uniform_Limit.thy` (diff)
The file was modified	`src/HOL/Analysis/Vitali_Covering_Theorem.thy` (diff)
The file was modified	`src/HOL/Bali/Basis.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Primes.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/MIR.thy` (diff)
The file was modified	`src/HOL/Hoare_Parallel/RG_Hoare.thy` (diff)
The file was modified	`src/HOL/Library/Countable_Complete_Lattices.thy` (diff)
The file was modified	`src/HOL/Library/Countable_Set_Type.thy` (diff)
The file was modified	`src/HOL/Library/Disjoint_Sets.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Nonnegative_Real.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Real.thy` (diff)
The file was modified	`src/HOL/Library/Finite_Map.thy` (diff)
The file was modified	`src/HOL/Library/Indicator_Function.thy` (diff)
The file was modified	`src/HOL/Library/Liminf_Limsup.thy` (diff)
The file was modified	`src/HOL/Library/Option_ord.thy` (diff)
The file was modified	`src/HOL/Library/Order_Continuity.thy` (diff)
The file was modified	`src/HOL/Library/Product_Order.thy` (diff)
The file was modified	`src/HOL/Library/Set_Algebras.thy` (diff)
The file was modified	`src/HOL/Library/Set_Idioms.thy` (diff)
The file was modified	`src/HOL/Library/Stream.thy` (diff)
The file was modified	`src/HOL/Probability/Fin_Map.thy` (diff)
The file was modified	`src/HOL/Probability/Independent_Family.thy` (diff)
The file was modified	`src/HOL/Probability/Probability_Mass_Function.thy` (diff)
The file was modified	`src/HOL/Probability/Projective_Family.thy` (diff)
The file was modified	`src/HOL/Probability/Stopping_Time.thy` (diff)
The file was modified	`src/HOL/Probability/Tree_Space.thy` (diff)
The file was modified	`src/HOL/Probability/ex/Measure_Not_CCC.thy` (diff)
The file was modified	`src/HOL/UNITY/Comp/Alloc.thy` (diff)
The file was modified	`src/HOL/UNITY/Comp/AllocBase.thy` (diff)
The file was modified	`src/HOL/UNITY/Comp/AllocImpl.thy` (diff)
The file was modified	`src/HOL/UNITY/Constrains.thy` (diff)
The file was modified	`src/HOL/UNITY/Extend.thy` (diff)
The file was modified	`src/HOL/UNITY/Guar.thy` (diff)
The file was modified	`src/HOL/UNITY/Lift_prog.thy` (diff)
The file was modified	`src/HOL/UNITY/Simple/Reachability.thy` (diff)
The file was modified	`src/HOL/UNITY/Union.thy` (diff)
Changeset 69312:e0f68a507683 by nipkow: added and tuned lemmas
The file was modified	`src/HOL/Finite_Set.thy` (diff)
The file was modified	`src/HOL/List.thy` (diff)