diff -r af34dd3418fe -r 2406350c358f Nominal/Ex3.thy
--- a/Nominal/Ex3.thy	Tue Mar 23 08:45:08 2010 +0100
+++ b/Nominal/Ex3.thy	Tue Mar 23 08:46:44 2010 +0100
@@ -2,6 +2,8 @@
 imports "Parser"
 begin
 
+(* Example 3, identical to example 1 from Terms.thy *)
+
 atom_decl name
 
 ML {* val _ = recursive := false  *}