--- a/Nominal/Ex/SFT/Theorem.thy	Fri Jun 24 10:30:06 2011 +0900
+++ b/Nominal/Ex/SFT/Theorem.thy	Fri Jun 24 10:54:31 2011 +0900
@@ -1,10 +1,8 @@
 header {* The main lemma about Num and the Second Fixed Point Theorem *}
 theory Theorem imports Consts begin
 
-(*<*)
 lemmas [simp] = b3[OF bI] b1 b4 b5 supp_Num[unfolded Num_def supp_ltgt] Num_def lam.fresh[unfolded fresh_def] fresh_def b6
 lemmas app = Ltgt1_app
-(*>*)
 
 lemma Num:
   shows "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>"
@@ -67,4 +65,5 @@
   also have "... = F \<cdot> \<lbrace>X\<rbrace>" unfolding X_def ..
   finally show ?thesis by blast
 qed
-(*>*)
+
+end