Changes

Summary

merged
removed session name
merged
NEWS
merged
summarized structural and ordering invariant for trees
Total correctness examples by Walter Guttmann
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
tuned

Changeset 72813:b09f358f3eb0 by Peter Lammich: merged
Changeset 72812:caf2fd14e28b by Peter Lammich: removed session name
The file was modified	`src/HOL/Data_Structures/Binomial_Heap.thy` (diff)
Changeset 72811:ef21a1de340d by nipkow: merged
Changeset 72810:b00ee476151b by nipkow: NEWS
The file was modified	`NEWS` (diff)
Changeset 72809:64d8a7e6d8fa by Peter Lammich: merged
Changeset 72808:ba65dc3e35af by Peter Lammich: summarized structural and ordering invariant for trees
The file was modified	`src/HOL/Data_Structures/Binomial_Heap.thy` (diff)
Changeset 72807:ea189da0ff60 by nipkow: Total correctness examples by Walter Guttmann
The file was added	`src/HOL/Hoare/ExamplesTC.thy`
Changeset 72806:4fa08e083865 by nipkow: Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
The file was modified	`CONTRIBUTORS` (diff)
The file was modified	`src/HOL/Hoare/Hoare.thy` (diff)
The file was modified	`src/HOL/Hoare/Hoare_Logic.thy` (diff)
The file was modified	`src/HOL/Hoare/Hoare_Logic_Abort.thy` (diff)
The file was modified	`src/HOL/Hoare/README.html` (diff)
The file was modified	`src/HOL/Hoare/SchorrWaite.thy` (diff)
The file was modified	`src/HOL/Hoare/hoare_syntax.ML` (diff)
The file was modified	`src/HOL/Hoare/hoare_tac.ML` (diff)
The file was modified	`src/HOL/Isar_Examples/Hoare.thy` (diff)
The file was modified	`src/HOL/Isar_Examples/Hoare_Ex.thy` (diff)
Changeset 72805:976d656ed31e by nipkow: tuned
The file was modified	`src/HOL/Data_Structures/Tree23_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree23_Set.thy` (diff)