96 use "Minisubpbl/000-comments.sml" |
96 use "Minisubpbl/000-comments.sml" |
97 use "Minisubpbl/100-init-rootpbl.sml" |
97 use "Minisubpbl/100-init-rootpbl.sml" |
98 use "Minisubpbl/150-add-given.sml" |
98 use "Minisubpbl/150-add-given.sml" |
99 use "Minisubpbl/200-start-method.sml" |
99 use "Minisubpbl/200-start-method.sml" |
100 use "Minisubpbl/300-init-subpbl.sml" |
100 use "Minisubpbl/300-init-subpbl.sml" |
101 ML {* |
|
102 |
|
103 *} |
|
104 ML {* |
|
105 *} |
|
106 ML {* |
|
107 *} |
|
108 ML {* |
|
109 *} |
|
110 ML {* |
|
111 *} |
|
112 ML {* |
|
113 *} |
|
114 use "Minisubpbl/400-start-meth-subpbl.sml" |
101 use "Minisubpbl/400-start-meth-subpbl.sml" |
115 use "Minisubpbl/500-postcond.sml" |
102 use "Minisubpbl/500-postcond.sml" |
|
103 |
|
104 ML {* |
|
105 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; |
|
106 val (dI',pI',mI') = |
|
107 ("Test", ["sqroot-test","univariate","equation","test"], |
|
108 ["Test","squ-equ-test-subpbl1"]); |
|
109 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
110 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
111 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
112 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
113 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
114 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
115 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
116 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
117 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
118 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
119 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*) |
|
120 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
121 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
122 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
123 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
124 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
125 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
126 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
127 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
128 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*); |
|
129 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*); |
|
130 *} |
|
131 ML {* |
|
132 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *); |
|
133 *} |
|
134 ML {* |
|
135 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
136 *} |
|
137 ML {* |
|
138 *} |
|
139 ML {* |
|
140 *} |
|
141 ML {* |
|
142 *} |
|
143 |
|
144 |
116 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*} |
145 ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*} |
117 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} |
146 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} |
118 use "Interpret/mstools.sml" (*new 2010*) |
147 use "Interpret/mstools.sml" (*new 2010*) |
119 ML {* |
148 ML {* |
120 (*test/../ctree.sml*) |
149 (*test/../ctree.sml*) |