equal
deleted
inserted
replaced
441 val discI_thms = |
441 val discI_thms = |
442 map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms |
442 map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms |
443 disc_defs'; |
443 disc_defs'; |
444 val not_discI_thms = |
444 val not_discI_thms = |
445 map2 (fn m => fn def => funpow m (fn thm => allI RS thm) |
445 map2 (fn m => fn def => funpow m (fn thm => allI RS thm) |
446 (unfold_defs lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) |
446 (unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]}))) |
447 ms disc_defs'; |
447 ms disc_defs'; |
448 |
448 |
449 val (disc_thmss', disc_thmss) = |
449 val (disc_thmss', disc_thmss) = |
450 let |
450 let |
451 fun mk_thm discI _ [] = refl RS discI |
451 fun mk_thm discI _ [] = refl RS discI |