src/HOL/Hoare/Hoare.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 35321 c298a4fc324b
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
haftmann@35316
     1
(*  Author:     Tobias Nipkow
nipkow@14028
     2
    Copyright   1998-2003 TUM
nipkow@1335
     3
*)
nipkow@1335
     4
haftmann@35316
     5
theory Hoare
haftmann@35316
     6
imports Examples ExamplesAbort Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation
haftmann@35316
     7
begin
haftmann@35316
     8
haftmann@35316
     9
end