1.1 --- a/test/Tools/isac/Test_Isac.thy Sun Oct 23 17:21:04 2022 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Oct 25 16:15:47 2022 +0200
1.3 @@ -138,13 +138,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" (*+*) (*+++*) (* keep for continuation*) (*isa*) (*isa2*) (**)
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 @@ -204,7 +234,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"