| changeset 15076 | 4b3d280ef06a |
| parent 14174 | f3cafd2929d5 |
| child 15097 | b807858b97bd |
--- a/src/HOL/MicroJava/J/WellForm.thy Thu Jul 22 19:33:12 2004 +0200 +++ b/src/HOL/MicroJava/J/WellForm.thy Mon Jul 26 15:48:50 2004 +0200 @@ -316,7 +316,7 @@ apply( assumption) apply( fast) apply(auto dest!: wf_cdecl_supD) -apply(erule (1) converse_rtrancl_into_rtrancl) +(*CBtrancl: apply(erule (1) converse_rtrancl_into_rtrancl) *) done lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"