equal
deleted
inserted
replaced
31 |
31 |
32 (* |
32 (* |
33 > val t = (term_of o the o (parse thy)) "#2^^^#3"; |
33 > val t = (term_of o the o (parse thy)) "#2^^^#3"; |
34 > val eval_fn = the (assoc (!eval_list, "pow")); |
34 > val eval_fn = the (assoc (!eval_list, "pow")); |
35 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t; |
35 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t; |
36 > Sign.string_of_term (sign_of thy) t'; |
36 > Syntax.string_of_term (thy2ctxt thy) t'; |
37 *) |
37 *) |
38 (******************************************************************) |
38 (******************************************************************) |
39 (* ------------------------------------- *) |
39 (* ------------------------------------- *) |
40 " _________________ equation with x =(-12)/5, but L ={} ------- "; |
40 " _________________ equation with x =(-12)/5, but L ={} ------- "; |
41 (* ------------------------------------- *) |
41 (* ------------------------------------- *) |