equal
deleted
inserted
replaced
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")*) |