1 header {* The main lemma about Num and the Second Fixed Point Theorem *}

     1 header {* The main lemma about Num and the Second Fixed Point Theorem *}

     2 theory Theorem imports Consts begin

     3 theory Theorem imports Consts begin

     3 

     4 

     4 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

     5 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

     5 lemmas app = Ltgt1_app

     6 lemmas app = Ltgt1_app

     6 

     7