74 fetchProposedTactic 1 (*'' in tacis*); |
74 fetchProposedTactic 1 (*'' in tacis*); |
75 val ((pt,p),tacis) = get_calc 1; |
75 val ((pt,p),tacis) = get_calc 1; |
76 val ip = get_pos 1 1; |
76 val ip = get_pos 1 1; |
77 val (Form f, tac, asms) = pt_extract (pt, p); |
77 val (Form f, tac, asms) = pt_extract (pt, p); |
78 if term2str f = "[x = 1]"andalso p = ([],Res) andalso ip = ([],Res)then()else |
78 if term2str f = "[x = 1]"andalso p = ([],Res) andalso ip = ([],Res)then()else |
79 raise error "tacis.sml: diff.behav. in fetchProposedTactic autoCalculate"; |
79 error "tacis.sml: diff.behav. in fetchProposedTactic autoCalculate"; |
80 |
80 |
81 |
81 |
82 |
82 |
83 "------ setNextTactic -> autoCalculate (Step1 ) ------------------"; |
83 "------ setNextTactic -> autoCalculate (Step1 ) ------------------"; |
84 "------ setNextTactic -> autoCalculate (Step1 ) ------------------"; |
84 "------ setNextTactic -> autoCalculate (Step1 ) ------------------"; |
93 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*); |
93 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*); |
94 |
94 |
95 setNextTactic 1 (Rewrite_Set "norm_equation"); |
95 setNextTactic 1 (Rewrite_Set "norm_equation"); |
96 val (_, tacis) = get_calc 1; |
96 val (_, tacis) = get_calc 1; |
97 case tacis of [(Rewrite_Set "norm_equation",_,(([1], Res), _))] => () | _ => |
97 case tacis of [(Rewrite_Set "norm_equation",_,(([1], Res), _))] => () | _ => |
98 raise error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (1)"; |
98 error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (1)"; |
99 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 + -1 * 2 = 0*); |
99 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 + -1 * 2 = 0*); |
100 |
100 |
101 setNextTactic 1 (Rewrite_Set "Test_simplify"); |
101 setNextTactic 1 (Rewrite_Set "Test_simplify"); |
102 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*); |
102 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*); |
103 val ((pt,_),_) = get_calc 1; |
103 val ((pt,_),_) = get_calc 1; |
122 |
122 |
123 setNextTactic 1 (Apply_Method ["Test", "solve_linear"]); |
123 setNextTactic 1 (Apply_Method ["Test", "solve_linear"]); |
124 val (_, tacis) = get_calc 1; |
124 val (_, tacis) = get_calc 1; |
125 case tacis of |
125 case tacis of |
126 [((Apply_Method ["Test","solve_linear"],_,(([3,1], Frm), _)))] =>() | _ => |
126 [((Apply_Method ["Test","solve_linear"],_,(([3,1], Frm), _)))] =>() | _ => |
127 raise error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (2)"; |
127 error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (2)"; |
128 (*#######################################################################*) |
128 (*#######################################################################*) |
129 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*); |
129 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*); |
130 |
130 |
131 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv")); |
131 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv")); |
132 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 0 + -1 * -1*); |
132 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 0 + -1 * -1*); |
147 ["sqroot-test","univariate","equation","test"]); |
147 ["sqroot-test","univariate","equation","test"]); |
148 val (_, tacis) = get_calc 1; |
148 val (_, tacis) = get_calc 1; |
149 |
149 |
150 (*case tacis of 040609 suddenly ???! |
150 (*case tacis of 040609 suddenly ???! |
151 [((Check_Postcond _, _,(([], Res), _)))] =>() | _ => |
151 [((Check_Postcond _, _,(([], Res), _)))] =>() | _ => |
152 raise error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (3)"; |
152 error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (3)"; |
153 #######################################################################*) |
153 #######################################################################*) |
154 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*); |
154 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*); |
155 |
155 |
156 val ((pt,p),tacis) = get_calc 1; |
156 val ((pt,p),tacis) = get_calc 1; |
157 val ip = get_pos 1 1; |
157 val ip = get_pos 1 1; |
158 val (Form f, tac, asms) = pt_extract (pt, p); |
158 val (Form f, tac, asms) = pt_extract (pt, p); |
159 if term2str f = "[x = 1]"andalso p = ([],Res) andalso ip = ([],Res)then()else |
159 if term2str f = "[x = 1]"andalso p = ([],Res) andalso ip = ([],Res)then()else |
160 raise error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (4)"; |
160 error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (4)"; |
161 |
161 |
162 |
162 |
163 |
163 |