src/HOL/Hoare/Hoare.thy
author wenzelm
Wed, 04 Dec 2013 18:59:20 +0100
changeset 54667 4dd08fe126ba
parent 35321 c298a4fc324b
child 72806 4fa08e083865
permissions -rw-r--r--
remove junk;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35316
870dfea4f9c0 dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents: 24584
diff changeset
     1
(*  Author:     Tobias Nipkow
14028
ff6eb32b30a1 eparation logic - a beginning.
nipkow
parents: 13875
diff changeset
     2
    Copyright   1998-2003 TUM
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     3
*)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     4
35316
870dfea4f9c0 dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents: 24584
diff changeset
     5
theory Hoare
870dfea4f9c0 dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents: 24584
diff changeset
     6
imports Examples ExamplesAbort Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation
870dfea4f9c0 dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents: 24584
diff changeset
     7
begin
870dfea4f9c0 dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents: 24584
diff changeset
     8
870dfea4f9c0 dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents: 24584
diff changeset
     9
end