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