src/HOL/Hoare/Hoare.thy
author wenzelm
Wed, 25 Jul 2012 18:05:07 +0200
changeset 48502 fd03877ad5bc
parent 35321 c298a4fc324b
child 72806 4fa08e083865
permissions -rw-r--r--
session specifications for doc-src, excluding TutorialI for now;
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