src/ZF/IMP/Com.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Com.ML	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,39 @@
+(*  Title: 	ZF/IMP/Com.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+structure Com = Datatype_Fun
+ (
+  val thy = Bexp.thy;
+  val thy_name = "Com";
+  val rec_specs = 
+      [
+       (
+        "com", "univ(aexp Un bexp)",
+	  [
+           (["skip"],		"i", NoSyn),
+	   ([":="],	"[i,i] => i", Infixl 60),
+	   ([";"],	"[i,i] => i", Infixl 60),
+	   (["whileC"], 	"[i,i] => i", Mixfix("while _ do _",[],60)),
+	   (["ifC"],		"[i,i,i] => i",
+              Mixfix("ifc _ then _ else _",[],60))
+          ]
+       )
+      ];
+
+  val rec_styp = "i";
+
+  val sintrs = 
+       [
+	"skip : com",
+	"[| x:loc; a:aexp|] ==> X(x) := a : com",
+	"[| c0:com; c1:com|] ==> c0 ; c1 : com",
+	"[| b:bexp; c:com|] ==> while b do c : com",
+	"[| b:bexp; c0:com; c1:com|] ==> ifc b then c0 else c1 : com"
+       ];
+  val monos = [];
+  val type_intrs = [e-mail];
+  val type_elims = datatype_elims
+ );