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