isabelle: src/HOL/Hoare/ROOT.ML@ff6eb32b30a1 (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1363 diff changeset	1	(* Title: HOL/IMP/ROOT.ML
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 1363 diff changeset	3	Author: Tobias Nipkow
14028 ff6eb32b30a1 eparation logic - a beginning. nipkow parents: 13875 diff changeset	4	Copyright 1998-2003 TUM
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	5	*)
5e1c0540f285 New directory. nipkow parents: diff changeset	6
9000 c20d58286a51 cleaned up; wenzelm parents: 6349 diff changeset	7	time_use_thy "Examples";
13857 11d7c5a8dbb7 * empty log message * nipkow parents: 13772 diff changeset	8	time_use_thy "ExamplesAbort";
13771 6cd59cc885a1 * empty log message * nipkow parents: 13132 diff changeset	9	time_use_thy "Pointers0";
13772 73d041cc6a66 Split Pointers.thy and automated one proof, which caused the runtime to explode nipkow parents: 13771 diff changeset	10	time_use_thy "Pointer_Examples";
13875 12997e3ddd8d * empty log message * nipkow parents: 13857 diff changeset	11	time_use_thy "Pointer_ExamplesAbort";
12997e3ddd8d * empty log message * nipkow parents: 13857 diff changeset	12	time_use_thy "SchorrWaite";
14028 ff6eb32b30a1 eparation logic - a beginning. nipkow parents: 13875 diff changeset	13	time_use_thy "Separation";