equal
deleted
inserted
replaced
356 fun nprems_of (Thm {prop, ...}) = |
356 fun nprems_of (Thm {prop, ...}) = |
357 Logic.count_prems (Logic.skip_flexpairs prop, 0); |
357 Logic.count_prems (Logic.skip_flexpairs prop, 0); |
358 |
358 |
359 fun major_prem_of thm = |
359 fun major_prem_of thm = |
360 (case prems_of thm of |
360 (case prems_of thm of |
361 prem :: _ => prem |
361 prem :: _ => Logic.strip_assums_concl prem |
362 | [] => raise THM ("major_prem_of: rule with no premises", 0, [thm])); |
362 | [] => raise THM ("major_prem_of: rule with no premises", 0, [thm])); |
363 |
363 |
364 fun no_prems thm = nprems_of thm = 0; |
364 fun no_prems thm = nprems_of thm = 0; |
365 |
365 |
366 (*maps object-rule to conclusion*) |
366 (*maps object-rule to conclusion*) |