src/HOL/MicroJava/J/TypeRel.thy
changeset 11088 08690b7c0568
parent 11070 cc421547e744
child 11266 70c9ebbffc49
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Feb 09 16:23:40 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Feb 09 20:34:42 2001 +0100
     1.3 @@ -189,8 +189,6 @@
     1.4  apply(erule (1) rtrancl_trans)
     1.5  done
     1.6  
     1.7 -ML {* InductAttrib.print_global_rules(the_context()) *}
     1.8 -ML {* set show_tags *}
     1.9  
    1.10  (*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
    1.11  proof -