| author | blanchet | 
| Mon, 30 Jan 2012 17:15:59 +0100 | |
| changeset 46368 | ded0390eceae | 
| parent 35321 | c298a4fc324b | 
| child 72806 | 4fa08e083865 | 
| permissions | -rw-r--r-- | 
| 
35316
 
870dfea4f9c0
dropped axclass; dropped Id; session theory Hoare.thy
 
haftmann 
parents: 
24584 
diff
changeset
 | 
1  | 
(* Author: Tobias Nipkow  | 
| 14028 | 2  | 
Copyright 1998-2003 TUM  | 
| 1335 | 3  | 
*)  | 
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  |