tuned decompose-isar
authorWalther Neuper <neuper@ist.tugraz.at>
Mon, 18 Jul 2011 16:39:22 +0200
branchdecompose-isar
changeset 421046879bed0ff4d
parent 42103 e921660e2d7c
child 42105 64f12a53d644
tuned
test/Tools/isac/Interpret/mathengine.sml
     1.1 --- a/test/Tools/isac/Interpret/mathengine.sml	Mon Jul 18 16:37:30 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/mathengine.sml	Mon Jul 18 16:39:22 2011 +0200
     1.3 @@ -414,6 +414,8 @@
     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)", "x = 1", "precond_rootmet x"]
     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";
    1.12