src/HOL/Hoare/Hoare.thy
author nipkow
Tue, 05 Nov 2019 14:57:41 +0100
changeset 71033 c1b63124245c
parent 35321 c298a4fc324b
child 72806 4fa08e083865
permissions -rw-r--r--
tuned
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