equal
deleted
inserted
replaced
36 autoCalculate 1 (Steps 1); |
36 autoCalculate 1 (Steps 1); |
37 val ((pt, p), _) = get_calc 1; show_pt pt; |
37 val ((pt, p), _) = get_calc 1; show_pt pt; |
38 val appltacs = specific_from_prog pt p; |
38 val appltacs = specific_from_prog pt p; |
39 case appltacs of |
39 case appltacs of |
40 [Rewrite ("radd_commute", radd_commute), |
40 [Rewrite ("radd_commute", radd_commute), |
41 Rewrite ("add_assoc", add_assoc), Calculate "TIMES"] |
41 Rewrite ("add.assoc", add_assoc), Calculate "TIMES"] |
42 => if (UnparseC.term o Thm.prop_of) radd_commute = "?m + ?n = ?n + ?m" andalso |
42 => if (UnparseC.term o Thm.prop_of) radd_commute = "?m + ?n = ?n + ?m" andalso |
43 (UnparseC.term o Thm.prop_of) add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then () |
43 (UnparseC.term o Thm.prop_of) add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then () |
44 else error "script.sml fun specific_from_prog diff.behav. 2" |
44 else error "script.sml fun specific_from_prog diff.behav. 2" |
45 | _ => error "script.sml fun specific_from_prog diff.behav. 1"; |
45 | _ => error "script.sml fun specific_from_prog diff.behav. 1"; |
46 |
46 |