equal
deleted
inserted
replaced
138 "~~~~~ fun xxx , args:"; val () = (); |
138 "~~~~~ fun xxx , args:"; val () = (); |
139 "~~~~~ and xxx , args:"; val () = (); |
139 "~~~~~ and xxx , args:"; val () = (); |
140 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = (); |
140 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = (); |
141 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*); |
141 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*); |
142 "xx" |
142 "xx" |
143 ^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**) |
143 ^ "xxx" (*+*) (*+++*) (* keep for continuation*) (*isa*) (*isa2*) (**) |
144 \<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*) |
144 \<close> ML \<open> (*//----------- adhoc inserted n ----------------------------------------------------\\*) |
145 \<close> ML \<open> |
145 (*//----------------- adhoc inserted n ----------------------------------------------------\\*) |
146 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*) |
146 (*\\------------------ adhoc inserted n ----------------------------------------------------//*) |
|
147 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*) |
147 \<close> |
148 \<close> |
148 ML \<open> |
149 ML \<open> |
149 \<close> ML \<open> |
150 \<close> ML \<open> |
150 \<close> ML \<open> |
151 \<close> ML \<open> |
151 \<close> ML \<open> |
152 \<close> ML \<open> |