--- a/src/ZF/IMP/Com.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/IMP/Com.thy Tue Nov 29 00:31:31 1994 +0100
@@ -96,7 +96,7 @@
translations
"<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
-rules
+defs
assign_def "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
inductive