Nominal/Ex/SFT/Theorem.thy
changeset 2898 a95a497e1f4f
parent 2894 8ec94871de1e
child 3087 c95afd0dc594
--- a/Nominal/Ex/SFT/Theorem.thy	Fri Jun 24 11:15:22 2011 +0900
+++ b/Nominal/Ex/SFT/Theorem.thy	Fri Jun 24 11:18:18 2011 +0900
@@ -1,4 +1,5 @@
 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