Changes

Summary

eliminated use of empty "assms";
more complete theories;

Changeset 63092:a949b2a5f51d by wenzelm: eliminated use of empty "assms";
The file was modified	`src/HOL/BNF_Def.thy` (diff)
The file was modified	`src/HOL/BNF_Wellorder_Constructions.thy` (diff)
The file was modified	`src/HOL/BNF_Wellorder_Embedding.thy` (diff)
The file was modified	`src/HOL/Binomial.thy` (diff)
The file was modified	`src/HOL/Cardinals/Cardinal_Order_Relation.thy` (diff)
The file was modified	`src/HOL/Conditionally_Complete_Lattices.thy` (diff)
The file was modified	`src/HOL/Deriv.thy` (diff)
The file was modified	`src/HOL/Equiv_Relations.thy` (diff)
The file was modified	`src/HOL/Groups_Big.thy` (diff)
The file was modified	`src/HOL/Imperative_HOL/ex/Linked_Lists.thy` (diff)
The file was modified	`src/HOL/Library/Complete_Partial_Order2.thy` (diff)
The file was modified	`src/HOL/Library/ContNotDenum.thy` (diff)
The file was modified	`src/HOL/Library/Convex.thy` (diff)
The file was modified	`src/HOL/Library/Countable_Set.thy` (diff)
The file was modified	`src/HOL/Library/Extended_Real.thy` (diff)
The file was modified	`src/HOL/Library/FSet.thy` (diff)
The file was modified	`src/HOL/Library/Fraction_Field.thy` (diff)
The file was modified	`src/HOL/Library/FuncSet.thy` (diff)
The file was modified	`src/HOL/Library/Indicator_Function.thy` (diff)
The file was modified	`src/HOL/Library/Multiset.thy` (diff)
The file was modified	`src/HOL/Library/Nonpos_Ints.thy` (diff)
The file was modified	`src/HOL/Lifting.thy` (diff)
The file was modified	`src/HOL/List.thy` (diff)
The file was modified	`src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy` (diff)
The file was modified	`src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy` (diff)
The file was modified	`src/HOL/Multivariate_Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Multivariate_Analysis/Integration.thy` (diff)
The file was modified	`src/HOL/Multivariate_Analysis/Path_Connected.thy` (diff)
The file was modified	`src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Cong.thy` (diff)
The file was modified	`src/HOL/Probability/Bochner_Integration.thy` (diff)
The file was modified	`src/HOL/Probability/Distribution_Functions.thy` (diff)
The file was modified	`src/HOL/Probability/Giry_Monad.thy` (diff)
The file was modified	`src/HOL/Probability/Interval_Integral.thy` (diff)
The file was modified	`src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy` (diff)
The file was modified	`src/HOL/Probability/Probability_Mass_Function.thy` (diff)
The file was modified	`src/HOL/Probability/Set_Integral.thy` (diff)
The file was modified	`src/HOL/SPARK/Tools/spark_commands.ML` (diff)
The file was modified	`src/HOL/Set_Interval.thy` (diff)
The file was modified	`src/HOL/Topological_Spaces.thy` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)
The file was modified	`src/HOL/Transfer.thy` (diff)
Changeset 63091:54f16a0a3069 by wenzelm: more complete theories;
The file was modified	`src/HOL/ROOT` (diff)