# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269324267 -3600
# Node ID d804729d6cf4ba9fc45210cf2a9f2670e3b53f00
# Parent  10573d05dd905a3ddacd78bceaf2915bfef9622f
Move the comment to appropriate place.

diff -r 10573d05dd90 -r d804729d6cf4 Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 23 07:04:14 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 23 07:04:27 2010 +0100
@@ -2,8 +2,6 @@
 imports "Parser" "../Attic/Prove"
 begin
 
-text {* example 1, equivalent to example 2 from Terms *}
-
 atom_decl name
 
 ML {* val _ = recursive := false *}
@@ -89,6 +87,8 @@
   then show "P c lm" by simp
 qed
 
+text {* example 1, equivalent to example 2 from Terms *}
+
 nominal_datatype lam =
   VAR "name"
 | APP "lam" "lam"