test/Tools/isac/Minisubpbl/000-comments.sml
author Walther Neuper <wneuper@ist.tugraz.at>
Wed, 07 Feb 2018 15:00:37 +0100
changeset 59357 17bc5920c2fb
parent 42020 38d2b4935341
child 60761 c3a97132157f
permissions -rw-r--r--
Isabelle2015->17: new negation "~ " --> "<not> "
     1 (* Title:  000-comments.sml
     2    Author: Walther Neuper 1105
     3    (c) copyright due to lincense terms.
     4 *)
     5 
     6 (* The tests in this directory use one specific example exclusively.
     7   The example uses data specifically defined in Test.thy exclusively.
     8   The example covers the essential features of isac's mathengine.
     9   Each test is kept in a separate file.
    10   The order of the files reflects the sequence of work done by the mathengine.
    11   Testruns showing errors on files indicate roughly the points of failure.
    12 
    13   The sequence is diveded into the following groups:
    14   100  initialisation of the rootproblem and specify phase
    15   200  start and execute the method of the rootproblem
    16   300  initialisation of a subproblem from script and specify phase
    17   400  start and execute the method of the subproblem
    18   490  last step of execution with next step Check_Postcond
    19   500  shift interpretation from sub-method to root-method
    20   550  found error in Check_Elementwise Assumptions
    21   600  check postconditions of subproblem and rootproblem
    22 *)