finished: make autocalc..CompleteCalc run with x+1=2 decompose-isar
authorWalther Neuper <neuper@ist.tugraz.at>
Mon, 18 Jul 2011 16:42:26 +0200
branchdecompose-isar
changeset 4210564f12a53d644
parent 42104 6879bed0ff4d
child 42106 43dbf705d2f0
finished: make autocalc..CompleteCalc run with x+1=2
test/Tools/isac/Interpret/mathengine.sml
     1.1 --- a/test/Tools/isac/Interpret/mathengine.sml	Mon Jul 18 16:39:22 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/mathengine.sml	Mon Jul 18 16:42:26 2011 +0200
     1.3 @@ -414,7 +414,7 @@
     1.4  if msg = "end-of-calculation" andalso c = [] andalso p = ([], Res) then ()
     1.5  else error "autoCalculate..CompleteCalc: final result";
     1.6  if terms2strs (get_assumptions_ pt p) = 
     1.7 -  ["matches (?a = ?b) (-1 + x = 0)", (*precond of submet*)
     1.8 +  ["matches (?a = ?b) (-1 + x = 0)", (*precond of submet*) 
     1.9     "x = 1",                          (*result of subpbl and rootpbl*)
    1.10     "precond_rootmet x"]              (*precond of rootmet*)
    1.11  then () else error "autoCalculate..CompleteCalc: ctxt at final result";