src/HOL/MicroJava/J/TypeRel.thy
changeset 11088 08690b7c0568
parent 11070 cc421547e744
child 11266 70c9ebbffc49
equal deleted inserted replaced
11087:5a40937c6c4d 11088:08690b7c0568
   187 apply  (frule_tac [2] widen_RefT)
   187 apply  (frule_tac [2] widen_RefT)
   188 apply  safe
   188 apply  safe
   189 apply(erule (1) rtrancl_trans)
   189 apply(erule (1) rtrancl_trans)
   190 done
   190 done
   191 
   191 
   192 ML {* InductAttrib.print_global_rules(the_context()) *}
       
   193 ML {* set show_tags *}
       
   194 
   192 
   195 (*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
   193 (*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
   196 proof -
   194 proof -
   197   assume "G\<turnstile>S\<preceq>U"
   195   assume "G\<turnstile>S\<preceq>U"
   198   thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
   196   thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)