44 > val s = |
44 > val s = |
45 "if #1 < Length [A = a * b, a // #2 = #2] \ |
45 "if #1 < Length [A = a * b, a // #2 = #2] \ |
46 \then make_fun (R, [make, function], no_met) A a_ [A = a * b, a // #2 = #2]\ |
46 \then make_fun (R, [make, function], no_met) A a_ [A = a * b, a // #2 = #2]\ |
47 \else hd [A = a * b, a // #2 = #2]"; |
47 \else hd [A = a * b, a // #2 = #2]"; |
48 |
48 |
49 > cterm_of (sign_of thy) t'; |
49 > (Thm.cterm thy) t'; |
50 > val t = (term_of o the o (parse thy)) s; |
50 > val t = (term_of o the o (parse thy)) s; |
51 > val eval_fn = the (assoc (!eval_list, op_)); |
51 > val eval_fn = the (assoc (!eval_list, op_)); |
52 > val (SOME(_,t')) = get_pair op_ eval_fn t; |
52 > val (SOME(_,t')) = get_pair op_ eval_fn t; |
53 val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#)) |
53 val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#)) |
54 val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm |
54 val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm |
90 > val t = (term_of o the o (parse thy)) s; |
90 > val t = (term_of o the o (parse thy)) s; |
91 > eval_Nth thmid op_ t; |
91 > eval_Nth thmid op_ t; |
92 |
92 |
93 > val eval_fn = the (assoc (!eval_list, op_)); |
93 > val eval_fn = the (assoc (!eval_list, op_)); |
94 > val (SOME(id,t')) = get_pair op_ eval_fn t; |
94 > val (SOME(id,t')) = get_pair op_ eval_fn t; |
95 > cterm_of (sign_of thy) t'; |
95 > (Thm.cterm thy) t'; |
96 val it = "Nth #2 [A = a * b, a // #2 = #2] = (a // #2 = #2)" |
96 val it = "Nth #2 [A = a * b, a // #2 = #2] = (a // #2 = #2)" |
97 *) |
97 *) |
98 |
98 |
99 |
99 |
100 (*17.6.00: calc_list instead eval_list*) |
100 (*17.6.00: calc_list instead eval_list*) |