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.
fixed broken (partial) proof
authorChristian Urban <urbanc@in.tum.de>
Sat, 16 Jan 2010 04:23:27 +0100
changeset 898 fe506cb64093
parent 897 464619898890
child 899 2468c0f2b276
fixed broken (partial) proof
Quot/Examples/LamEx.thy file | annotate | diff | comparison | revisions 
--- a/Quot/Examples/LamEx.thy	Sat Jan 16 03:56:00 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Sat Jan 16 04:23:27 2010 +0100
@@ -464,14 +464,6 @@
 apply(case_tac "a=b")
 apply(clarify)
 apply(simp)
-apply(subst pt_swap_bij'')
-apply(rule pt_name_inst)
-apply(rule at_name_inst)
-apply(subst pt_swap_bij'')
-apply(rule pt_name_inst)
-apply(rule at_name_inst)
-apply(simp)
-apply(generate_fresh "name")
 (* probably true *)
 sorry
nominal2