diff -r fd4fa6df22d1 -r a95a497e1f4f Nominal/Ex/SFT/Theorem.thy --- 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