src/HOL/Nominal/Examples/SN.thy

--- a/src/HOL/Nominal/Examples/SN.thy	Mon Nov 28 00:25:43 2005 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Mon Nov 28 05:03:00 2005 +0100
@@ -1,10 +1,12 @@
 (* $Id$ *)
 
+
+
 theory sn
 imports lam_substs  Accessible_Part
 begin
 
-(* Strong normalisation according to the P&T book by Girard et al *)
+text {* Strong Normalisation proof from the Proofs and Types book *}
 
 section {* Beta Reduction *}