# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263612207 -3600
# Node ID fe506cb64093d75180f5fdea5e7b999a5289a65d
# Parent  4646198988909cf35bf26b5dfbe71d15a2a4da88
fixed broken (partial) proof

diff -r 464619898890 -r fe506cb64093 Quot/Examples/LamEx.thy
--- 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