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.
tests
authorChristian Urban <urbanc@in.tum.de>
Tue, 27 Jul 2010 23:34:30 +0200
changeset 2386 b1b648933850
parent 2385 fe25a3ffeb14
child 2387 082d9fd28f89
tests
Nominal/Ex/SingleLet.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/SingleLet.thy	Tue Jul 27 14:37:59 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Tue Jul 27 23:34:30 2010 +0200
@@ -58,34 +58,49 @@
   "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw"
   "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw"
   "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw"
-apply(auto)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule refl)
+apply(assumption)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(assumption)
 apply(assumption)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2)
-apply(simp add: a1)
+apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps)
+apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
 apply(rule_tac x="0" in exI)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
+apply(simp only: fun_rel_def)
+apply(rule allI | rule impI)+
 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
 apply(rule_tac x="0" in exI)
 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
-apply(rule refl)
+apply(assumption)
 done
 
 lemma [quot_respect]:
nominal2