| changeset 15097 | b807858b97bd |
| parent 15076 | 4b3d280ef06a |
| child 15481 | fc075ae929e4 |
--- a/src/HOL/MicroJava/J/WellForm.thy Mon Aug 02 10:12:02 2004 +0200 +++ b/src/HOL/MicroJava/J/WellForm.thy Mon Aug 02 10:15:37 2004 +0200 @@ -316,7 +316,6 @@ apply( assumption) apply( fast) apply(auto dest!: wf_cdecl_supD) -(*CBtrancl: apply(erule (1) converse_rtrancl_into_rtrancl) *) done lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"