src/HOL/IMP/Examples.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Examples.thy	Tue Jul 04 14:04:56 2000 +0200
@@ -0,0 +1,20 @@
+(*  Title:      HOL/IMP/Examples.thy
+    ID:         $Id$
+    Author:     David von Oheimb, TUM
+    Copyright   2000 TUM
+*)
+
+Examples = Natural +
+
+defs (* bring up the deferred definition for update *)
+
+ update_def "update == fun_upd"
+
+constdefs
+  
+  factorial :: loc => loc => com
+ "factorial a b == b :== (%s. 1);
+               WHILE (%s. s a ~= 0) DO
+                 (b :== (%s. s b * s a); a :== (%s. s a - 1))"
+  
+end