equal
deleted
inserted
replaced
20 [Thm.proof_of thm] [] of |
20 [Thm.proof_of thm] [] of |
21 [name] => name |
21 [name] => name |
22 | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm)); |
22 | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm)); |
23 |
23 |
24 fun prf_of thm = |
24 fun prf_of thm = |
25 let |
25 Reconstruct.proof_of thm |
26 val thy = Thm.theory_of_thm thm; |
26 |> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)]; (* FIXME *) |
27 val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm); |
|
28 in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *) |
|
29 |
27 |
30 fun subsets [] = [[]] |
28 fun subsets [] = [[]] |
31 | subsets (x::xs) = |
29 | subsets (x::xs) = |
32 let val ys = subsets xs |
30 let val ys = subsets xs |
33 in ys @ map (cons x) ys end; |
31 in ys @ map (cons x) ys end; |