equal
deleted
inserted
replaced
58 type T = Rule.program |
58 type T = Rule.program |
59 |
59 |
60 datatype leaf = Tac of term | Expr of term |
60 datatype leaf = Tac of term | Expr of term |
61 fun rep_stacexpr (Tac t ) = t |
61 fun rep_stacexpr (Tac t ) = t |
62 | rep_stacexpr (Expr t) = |
62 | rep_stacexpr (Expr t) = |
63 raise ERROR ("rep_stacexpr called with t= " ^ UnparseC.term t); |
63 raise ERROR ("rep_stacexpr called with t= " ^ TermC.unparse_ERROR t); |
64 |
64 |
65 (* the lucas-interpreter LI requires programs in this specific format *) |
65 (* the lucas-interpreter LI requires programs in this specific format *) |
66 fun prep_program thm = (thm |
66 fun prep_program thm = (thm |
67 |> Thm.prop_of |
67 |> Thm.prop_of |
68 |> HOLogic.dest_Trueprop |
68 |> HOLogic.dest_Trueprop |