src/ZF/Resid/Conversion.thy
changeset 11319 8b84ee2cc79c
parent 1478 2b8c2a7547ab
--- a/src/ZF/Resid/Conversion.thy	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Conversion.thy	Mon May 21 14:51:46 2001 +0200
@@ -29,7 +29,7 @@
   domains       "Sconv" <= "lambda*lambda"
   intrs
     one_step    "m<-1->n  ==> m<--->n"
-    refl        "m:lambda ==> m<--->m"
+    refl        "m \\<in> lambda ==> m<--->m"
     trans       "[|m<--->n; n<--->p|] ==> m<--->p"
   type_intrs    "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
 end