Example from HOLCF paper.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IMP/HoareEx.ML	Tue Sep 09 12:09:06 1997 +0200
@@ -0,0 +1,19 @@
+(*  Title:      HOLCF/IMP/HoareEx.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1997 TUM
+
+Correctness of while-loop.
+*)
+
+val prems = goalw thy [hoare_valid_def]
+"|= {A} c {A} ==> |= {A} WHILE b DO c {%s. A s & ~b s}";
+by(cut_facts_tac prems 1);
+by (Simp_tac 1);
+by (rtac fix_ind 1);
+  (* simplifier with enhanced adm-tactic: *)
+  by (Simp_tac 1);
+ by (Simp_tac 1);
+by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by(Blast_tac 1);
+qed "WHILE_rule_sound";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IMP/HoareEx.thy	Tue Sep 09 12:09:06 1997 +0200
@@ -0,0 +1,18 @@
+(*  Title:      HOLCF/IMP/HoareEx.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow, TUM
+    Copyright   1997 TUM
+
+An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch.
+It demonstrates fixpoint reasoning by showing the correctness of the Hoare
+rule for while-loops.
+*)
+
+HoareEx = Denotational +
+
+types assn = state => bool
+
+constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
+ "|= {A} c {B} == !s t. A s & D c `(Discr s) = Def t --> B t"
+
+end