diff -r ca9f84786137 -r baf06b1b2aaa test/Tools/isac/Test_Isac_Short.thy
--- a/test/Tools/isac/Test_Isac_Short.thy	Sun Oct 23 17:21:04 2022 +0200
+++ b/test/Tools/isac/Test_Isac_Short.thy	Tue Oct 25 16:15:47 2022 +0200
@@ -139,13 +139,43 @@
 "~~~~~ fun xxx , args:"; val () = ();
 "~~~~~ and xxx , args:"; val () = ();
 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
+"~~~~~ continue fun xxx"; val () = ();
 (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);
 "xx"
-^ "xxx"   (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)
+^ "xxx"   (*+*) (*+++*) (*keep for continuing XXXXX*) (*isa*) (*isa2*) (**)
 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*)
  (*//----------------- adhoc inserted n ----------------------------------------------------\\*)
 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)
 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
+
+\<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
+(*//------------------ step into XXXXX -----------------------------------------------------\\*)
+(*keep for continuing XXXXX*)
+\<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)
+(*-------------------- continuing XXXXX ------------------------------------------------------*)
+(*kept for continuing XXXXX*)
+(*-------------------- stop step into XXXXX --------------------------------------------------*)
+\<close> ML \<open> (*------------- stop step into XXXXX --------------------------------------------------*)
+(*\\------------------ step into XXXXX -----------------------------------------------------//*)
+\<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
+
+(*/------------------- check entry to XXXXX -------------------------------------------------\*)
+(*\------------------- check entry to XXXXX -------------------------------------------------/*)
+(*/------------------- check within XXXXX ---------------------------------------------------\*)
+(*\------------------- check within XXXXX ---------------------------------------------------/*)
+(*/------------------- check result of XXXXX ------------------------------------------------\*)
+(*\------------------- check result of XXXXX ------------------------------------------------/*)
+(* final test ... ----------------------------------------------------------------------------*)
+
+\<close> ML \<open> (*//----------- inserted hidden code ------------------------------------------------\\*)
+(*//------------------ inserted hidden code ------------------------------------------------\\*)
+(*\\------------------ inserted hidden code ------------------------------------------------//*)
+\<close> ML \<open> (*\\----------- inserted hidden code ------------------------------------------------//*)
+
+\<close> ML \<open> (*//----------- build new fun XXXXX -------------------------------------------------\\*)
+(*//------------------ build new fun XXXXX -------------------------------------------------\\*)
+(*\\------------------ build new fun XXXXX -------------------------------------------------//*)
+\<close> ML \<open> (*\\----------- build new fun XXXXX -------------------------------------------------//*)
 \<close>
 ML \<open>
 \<close> ML \<open>
@@ -205,7 +235,8 @@
 subsection \<open>basic functionality on simple example first\<close>
   ML_file "Minisubpbl/000-comments.sml"
   ML_file "Minisubpbl/100-init-rootpbl.sml"
-  ML_file "Minisubpbl/150-add-given.sml"
+  ML_file "Minisubpbl/150a-add-given-Maximum.sml"
+  ML_file "Minisubpbl/150b-add-given-Equation.sml"
   ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"
   ML_file "Minisubpbl/200-start-method.sml"
   ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"