1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Sun Oct 23 17:21:04 2022 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Tue Oct 25 16:15:47 2022 +0200
     1.3 @@ -139,13 +139,43 @@
     1.4  "~~~~~ fun xxx , args:"; val () = ();
     1.5  "~~~~~ and xxx , args:"; val () = ();
     1.6  "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
     1.7 +"~~~~~ continue fun xxx"; val () = ();
     1.8  (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);
     1.9  "xx"
    1.10 -^ "xxx"   (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)
    1.11 +^ "xxx"   (*+*) (*+++*) (*keep for continuing XXXXX*) (*isa*) (*isa2*) (**)
    1.12  \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
    1.13   (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
    1.14  (*\\------------------ adhoc inserted n ----------------------------------------------------//*)
    1.15  \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
    1.16 +
    1.17 +\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
    1.18 +(*//------------------ step into XXXXX -----------------------------------------------------\\*)
    1.19 +(*keep for continuing XXXXX*)
    1.20 +\<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)
    1.21 +(*-------------------- continuing XXXXX ------------------------------------------------------*)
    1.22 +(*kept for continuing XXXXX*)
    1.23 +(*-------------------- stop step into XXXXX --------------------------------------------------*)
    1.24 +\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)
    1.25 +(*\\------------------ step into XXXXX -----------------------------------------------------//*)
    1.26 +\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
    1.27 +
    1.28 +(*/------------------- check entry to XXXXX -------------------------------------------------\*)
    1.29 +(*\------------------- check entry to XXXXX -------------------------------------------------/*)
    1.30 +(*/------------------- check within XXXXX ---------------------------------------------------\*)
    1.31 +(*\------------------- check within XXXXX ---------------------------------------------------/*)
    1.32 +(*/------------------- check result of XXXXX ------------------------------------------------\*)
    1.33 +(*\------------------- check result of XXXXX ------------------------------------------------/*)
    1.34 +(* final test ... ----------------------------------------------------------------------------*)
    1.35 +
    1.36 +\<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)
    1.37 +(*//------------------ inserted hidden code ------------------------------------------------\\*)
    1.38 +(*\\------------------ inserted hidden code ------------------------------------------------//*)
    1.39 +\<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
    1.40 +
    1.41 +\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)
    1.42 +(*//------------------ build new fun XXXXX -------------------------------------------------\\*)
    1.43 +(*\\------------------ build new fun XXXXX -------------------------------------------------//*)
    1.44 +\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)
    1.45  \<close>
    1.46  ML \<open>
    1.47  \<close> ML \<open>
    1.48 @@ -205,7 +235,8 @@
    1.49  subsection \<open>basic functionality on simple example first\<close>
    1.50    ML_file "Minisubpbl/000-comments.sml"
    1.51    ML_file "Minisubpbl/100-init-rootpbl.sml"
    1.52 -  ML_file "Minisubpbl/150-add-given.sml"
    1.53 +  ML_file "Minisubpbl/150a-add-given-Maximum.sml"
    1.54 +  ML_file "Minisubpbl/150b-add-given-Equation.sml"
    1.55    ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"
    1.56    ML_file "Minisubpbl/200-start-method.sml"
    1.57    ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"