equal
deleted
inserted
replaced
133 |
133 |
134 ML \<open> |
134 ML \<open> |
135 "~~~~~ fun xxx , args:"; val () = (); |
135 "~~~~~ fun xxx , args:"; val () = (); |
136 "~~~~~ and xxx , args:"; val () = (); |
136 "~~~~~ and xxx , args:"; val () = (); |
137 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = (); |
137 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = (); |
138 (*if*) (*then*); (*else*); (*case*) (*of*); (*return from xxx*); |
138 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*); |
139 "xx" |
139 "xx" |
140 ^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**) |
140 ^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**) |
141 \<close> ML \<open> |
141 \<close> ML \<open> |
142 \<close> |
142 \<close> |
143 ML \<open> |
143 ML \<open> |
317 ML_file "BridgeLibisabelle/use-cases.sml" |
317 ML_file "BridgeLibisabelle/use-cases.sml" |
318 |
318 |
319 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
319 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
320 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
320 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
321 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
321 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
322 ML \<open>\<close> ML \<open> |
322 ML \<open> |
|
323 \<close> ML \<open> |
323 \<close> ML \<open> |
324 \<close> ML \<open> |
324 \<close> ML \<open> |
325 \<close> ML \<open> |
325 \<close> ML \<open> |
326 \<close> ML \<open> |
326 \<close> ML \<open> |
327 \<close> ML \<open> |
327 \<close> ML \<open> |
328 \<close> ML \<open> |