Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 16 Jun 2011 23:11:50 +0900
changeset 2867 39ae45d3a11b
parent 2866 9f667f6da04f
child 2868 2b8e387d2dfc
child 2869 9c0df9901acf
Fix
Nominal/Ex/TypeSchemes.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/TypeSchemes.thy	Thu Jun 16 22:00:52 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Jun 16 23:11:50 2011 +0900
@@ -197,6 +197,7 @@
 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")
 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")
+apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', Ta))")
 prefer 2
 apply (simp add: eqvt_at_def subst_def)
 apply rule
@@ -215,12 +216,12 @@
 apply (rule_tac x="lookup \<theta> X" in exI)
 apply clarify
 apply (rule the1_equality)
-apply metis apply assumption
+apply blast apply assumption
 apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))
                   (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)
 apply clarify
 apply (rule the1_equality)
-apply metis apply assumption
+apply blast apply assumption
 apply clarify
 apply simp
 --"-"
nominal2