tuned;
authorwenzelm
Fri Feb 09 20:34:42 2001 +0100 (2001-02-09)
changeset 1108808690b7c0568
parent 11087 5a40937c6c4d
child 11089 0f6f1cd500e5
tuned;
src/HOL/MicroJava/J/TypeRel.thy
     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 -