Changes

Summary

merged
isabelle emacs no longer exists;
utilize 'flip'
comments

Changeset 68408:9a2453622596 by wenzelm: merged
Changeset 68407:fd61a2e4e1f9 by wenzelm: isabelle emacs no longer exists;
The file was modified	`src/HOL/SPARK/Manual/Example_Verification.thy` (diff)
Changeset 68406:6beb45f6cf67 by nipkow: utilize 'flip'
The file was modified	`src/HOL/Library/BigO.thy` (diff)
The file was modified	`src/HOL/Library/Cardinality.thy` (diff)
The file was modified	`src/HOL/Library/Countable.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_Nat.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/Float.thy` (diff)
The file was modified	`src/HOL/Library/Going_To_Filter.thy` (diff)
The file was modified	`src/HOL/Library/Infinite_Set.thy` (diff)
The file was modified	`src/HOL/Library/Landau_Symbols.thy` (diff)
The file was modified	`src/HOL/Library/Lattice_Algebras.thy` (diff)
The file was modified	`src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy` (diff)
The file was modified	`src/HOL/Library/Log_Nat.thy` (diff)
The file was modified	`src/HOL/Library/Multiset.thy` (diff)
The file was modified	`src/HOL/Library/Multiset_Permutations.thy` (diff)
The file was modified	`src/HOL/Library/Periodic_Fun.thy` (diff)
The file was modified	`src/HOL/Library/Perm.thy` (diff)
The file was modified	`src/HOL/Library/Stirling.thy` (diff)
The file was modified	`src/HOL/Library/Stream.thy` (diff)
The file was modified	`src/HOL/Library/Sublist.thy` (diff)
The file was modified	`src/HOL/Library/Uprod.thy` (diff)
Changeset 68405:6a0852b8e5a8 by nipkow: comments
The file was modified	`src/Pure/raw_simplifier.ML` (diff)