diff -r 345e495d3b92 -r a7a537e0413a src/HOL/Nominal/Examples/VC_Condition.thy
--- a/src/HOL/Nominal/Examples/VC_Condition.thy	Sun Feb 10 20:49:48 2008 +0100
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy	Mon Feb 11 15:19:17 2008 +0100
@@ -27,6 +27,7 @@
   equivalence. However as a relation 'unbind' is ok and     
   a similar relation has been used in our formalisation 
   of the algorithm W. *}
+
 inductive
   unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60)
 where
@@ -38,6 +39,7 @@
   We can show that Lam [x].Lam [x].Var x unbinds to [x,x],Var x 
   and also to [z,y],Var y (though the proof for the second is a 
   bit clumsy). *} 
+
 lemma unbind_lambda_lambda1: 
   shows "Lam [x].Lam [x].(Var x)\<mapsto>[x,x],(Var x)"
 by (auto intro: unbind.intros)
@@ -74,6 +76,7 @@
   To obtain a faulty lemma, we introduce the function 'bind'
   which takes a list of names and abstracts them away in 
   a given lambda-term. *}
+
 fun 
   bind :: "name list \<Rightarrow> lam \<Rightarrow> lam"
 where
@@ -83,6 +86,7 @@
 text {*
   Although not necessary for our main argument below, we can 
   easily prove that bind undoes the unbinding. *}
+
 lemma bind_unbind:
   assumes a: "t \<mapsto> xs,t'"
   shows "t = bind xs t'"
@@ -93,6 +97,7 @@
   variable in t, and x does not occur in xs, then x is a free 
   variable in bind xs t. In the nominal tradition we formulate    
   'is a free variable in' as 'is not fresh for'. *}
+
 lemma free_variable:
   fixes x::"name"
   assumes a: "\<not>(x\<sharp>t)" and b: "x\<sharp>xs"
@@ -119,8 +124,8 @@
 text {*
   Obviously this lemma is bogus. For example, in 
   case Lam [x].Lam [x].(Var x) \<mapsto> [x,x],(Var x). 
-  As a result, we can prove False. 
-*}
+  As a result, we can prove False. *}
+
 lemma false1:
   shows "False"
 proof -
@@ -147,8 +152,8 @@
 
 text {* 
   The relation is equivariant but we have to use again 
-  sorry to derive a strong induction principle. 
-*}
+  sorry to derive a strong induction principle. *}
+
 equivariance strip
 
 nominal_inductive strip
@@ -156,8 +161,8 @@
 
 text {*
   The second faulty lemma shows that a variable being fresh
-  for a term is also fresh for this term after striping. 
-*}
+  for a term is also fresh for this term after striping. *}
+
 lemma faulty2:
   fixes x::"name"
   assumes a: "t \<rightarrow> t'"
@@ -167,6 +172,7 @@
    (auto simp add: abs_fresh)
 
 text {* Obviously Lam [x].Var x is a counter example to this lemma. *}
+
 lemma false2:
   shows "False"
 proof -
@@ -176,5 +182,11 @@
   ultimately have "x\<sharp>(Var x)" by (simp only: faulty2)
   then show "False" by (simp add: fresh_atm)
 qed 
+
+text {*
+  Moral: Who would have thought that the variable convention 
+  is in general an unsound reasoning principle.
+  *}
+
  
 end
\ No newline at end of file