equal
deleted
inserted
replaced
448 fun tpairs_of (Thm {tpairs, ...}) = tpairs; |
448 fun tpairs_of (Thm {tpairs, ...}) = tpairs; |
449 |
449 |
450 val concl_of = Logic.strip_imp_concl o prop_of; |
450 val concl_of = Logic.strip_imp_concl o prop_of; |
451 val prems_of = Logic.strip_imp_prems o prop_of; |
451 val prems_of = Logic.strip_imp_prems o prop_of; |
452 fun nprems_of th = Logic.count_prems (prop_of th, 0); |
452 fun nprems_of th = Logic.count_prems (prop_of th, 0); |
453 val no_prems = equal 0 o nprems_of; |
453 fun no_prems th = nprems_of th = 0; |
454 |
454 |
455 fun major_prem_of th = |
455 fun major_prem_of th = |
456 (case prems_of th of |
456 (case prems_of th of |
457 prem :: _ => Logic.strip_assums_concl prem |
457 prem :: _ => Logic.strip_assums_concl prem |
458 | [] => raise THM ("major_prem_of: rule with no premises", 0, [th])); |
458 | [] => raise THM ("major_prem_of: rule with no premises", 0, [th])); |