811 =========================================================================/ |
811 =========================================================================/ |
812 |
812 |
813 |
813 |
814 |
814 |
815 -----fun refin' ff: |
815 -----fun refin' ff: |
816 > (writeln o (itms2str Isac.thy)) itms; |
816 > (writeln o (itms2str_ (thy2ctxt "Isac"))) itms; |
817 [ |
817 [ |
818 (1 ,[1] ,true ,#Given ,Cor equalities |
818 (1 ,[1] ,true ,#Given ,Cor equalities |
819 [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2, |
819 [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2, |
820 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] ,(es_, [[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2, |
820 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] ,(es_, [[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2, |
821 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]])), |
821 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]])), |
826 [ |
826 [ |
827 (false, length_ es_ = 2), |
827 (false, length_ es_ = 2), |
828 (true, length_ [c, c_2] = 2)] |
828 (true, length_ [c, c_2] = 2)] |
829 |
829 |
830 ----- fun match_oris': |
830 ----- fun match_oris': |
831 > (writeln o (itms2str Isac.thy)) itms; |
831 > (writeln o (itms2str_ (thy2ctxt "Isac"))) itms; |
832 > (writeln o pres2str) pre'; |
832 > (writeln o pres2str) pre'; |
833 ..as in refin' |
833 ..as in refin' |
834 |
834 |
835 ----- fun check_preconds' |
835 ----- fun check_preconds' |
836 > (writeln o env2str) env; |
836 > (writeln o env2str) env; |
893 case nxt of |
893 case nxt of |
894 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () |
894 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () |
895 | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution"; |
895 | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution"; |
896 |
896 |
897 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
897 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
898 val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl; |
898 val PblObj {probl,...} = get_obj I pt [5]; |
|
899 (writeln o (itms2str_ (thy2ctxt "Isac"))) probl; |
899 (*[ |
900 (*[ |
900 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])), |
901 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])), |
901 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])), |
902 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])), |
902 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))] |
903 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))] |
903 *) |
904 *) |
961 case nxt of |
962 case nxt of |
962 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () |
963 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () |
963 | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution b"; |
964 | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution b"; |
964 |
965 |
965 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
966 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
966 val PblObj {probl,...} = get_obj I pt [5];(writeln o(itms2str Isac.thy)) probl; |
967 val PblObj {probl,...} = get_obj I pt [5]; |
|
968 (writeln o (itms2str_ (thy2ctxt "Isac"))) probl; |
967 (*[ |
969 (*[ |
968 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])), |
970 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])), |
969 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])), |
971 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])), |
970 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))] |
972 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))] |
971 *) |
973 *) |