1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Mon Apr 26 14:16:35 2021 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Tue Apr 27 18:09:22 2021 +0200
     1.3 @@ -135,7 +135,7 @@
     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 -(*if*) (*then*); (*else*);   (*case*) (*of*);  (*return from xxx*);
     1.8 +(*if*) (*then*); (*else*);   (*case*) (*of*);  (*return value*); (*in*) (*end*);
     1.9  "xx"
    1.10  ^ "xxx"   (*+*) (*!for return!*) (*isa*) (*REP*) (**)
    1.11  \<close> ML \<open>
    1.12 @@ -319,7 +319,8 @@
    1.13    ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
    1.14    ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
    1.15    ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
    1.16 -ML \<open>\<close> ML \<open>
    1.17 +ML \<open>
    1.18 +\<close> ML \<open>
    1.19  \<close> ML \<open>
    1.20  \<close> ML \<open>
    1.21  \<close> ML \<open>