equal
deleted
inserted
replaced
283 apply (rule lam2_fast_app, rule Lam_A, simp_all) |
283 apply (rule lam2_fast_app, rule Lam_A, simp_all) |
284 apply (rule lam3_fast_app, rule Lam_A, simp_all) |
284 apply (rule lam3_fast_app, rule Lam_A, simp_all) |
285 apply (rule lam2_fast_app, rule Lam_A, simp_all) |
285 apply (rule lam2_fast_app, rule Lam_A, simp_all) |
286 done |
286 done |
287 |
287 |
288 definition "Num \<equiv> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>" |
288 definition "NUM \<equiv> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>" |
289 |
289 |
290 lemma supp_Num[simp]: |
290 lemma supp_NUM[simp]: |
291 "supp Num = {}" |
291 "supp NUM = {}" |
292 by (auto simp only: Num_def supp_ltgt supp_Pair supp_A supp_Cons supp_Nil) |
292 by (auto simp only: NUM_def supp_ltgt supp_Pair supp_A supp_Cons supp_Nil) |
293 |
293 |
294 end |
294 end |