--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/IMP/Assign.thy	Thu Jul 21 14:27:00 1994 +0200
@@ -0,0 +1,13 @@
+(*  Title: 	ZF/IMP/Assign.thy
+    ID:         $Id$
+    Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
+    Copyright   1994 TUM
+*)
+
+Assign = Aexp +
+consts 
+	"assign" :: "[i,i,i] => i"	("_[_'/_]" [900,0,0] 900)
+
+rules 
+	assign_def	"sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
+end