src/ZF/IMP/Assign.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Assign.ML	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,12 @@
+(*  Title: 	ZF/IMP/Assign.ML
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+open Assign;
+
+val assign_type = prove_goalw Assign.thy [assign_def]
+	"[| sigma:loc -> nat; n:nat |] ==> sigma[n/x] : loc -> nat"
+    (fn prems => [(fast_tac  
+                   (ZF_cs addIs [apply_type,lam_type,if_type]@prems) 1)]);