# HG changeset patch
# User urbanc
# Date 1201504471 -3600
# Node ID 9fce1718825f4ff525cd9a003b42b818c10cb4ae
# Parent  21b51f748dafeefcbdacf4795fe42dec1adba2b4
tuned the proof of the substitution lemma

diff -r 21b51f748daf -r 9fce1718825f src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Sun Jan 27 22:21:39 2008 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Mon Jan 28 08:14:31 2008 +0100
@@ -104,16 +104,16 @@
     moreover 
     { (*Case 1.2*)
       assume "z=y" and "z\<noteq>x" 
-      have "(1)": "?LHS = L"               using `z\<noteq>x` `z=y` by force
-      have "(2)": "?RHS = L[x::=N[y::=L]]" using `z=y` by force
+      have "(1)": "?LHS = L"               using `z\<noteq>x` `z=y` by simp
+      have "(2)": "?RHS = L[x::=N[y::=L]]" using `z=y` by simp
       have "(3)": "L[x::=N[y::=L]] = L"    using `x\<sharp>L` by (simp add: forget)
       from "(1)" "(2)" "(3)" have "?LHS = ?RHS" by simp
     }
     moreover 
     { (*Case 1.3*)
       assume "z\<noteq>x" and "z\<noteq>y"
-      have "(1)": "?LHS = Var z" using `z\<noteq>x` `z\<noteq>y` by force
-      have "(2)": "?RHS = Var z" using `z\<noteq>x` `z\<noteq>y` by force
+      have "(1)": "?LHS = Var z" using `z\<noteq>x` `z\<noteq>y` by simp
+      have "(2)": "?RHS = Var z" using `z\<noteq>x` `z\<noteq>y` by simp
       from "(1)" "(2)" have "?LHS = ?RHS" by simp
     }
     ultimately show "?LHS = ?RHS" by blast