329 "----- test 4b false"; |
329 "----- test 4b false"; |
330 val tm = TermC.str2term "M_b x"; |
330 val tm = TermC.str2term "M_b x"; |
331 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 4" |
331 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 4" |
332 else (); |
332 else (); |
333 |
333 |
334 "----------- fun TermC.matches, repair 'Handler catches all exceptions' ------------------------------"; |
|
335 "----------- fun TermC.matches, repair 'Handler catches all exceptions' ------------------------------"; |
|
336 "----------- fun TermC.matches, repair 'Handler catches all exceptions' ------------------------------"; |
|
337 |
|
338 |
|
339 |
|
340 |
|
341 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------"; |
334 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------"; |
342 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------"; |
335 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------"; |
343 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------"; |
336 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------"; |
344 (* added after Isabelle2015->17 |
337 (* added after Isabelle2015->17 |
345 > val (SOME ct) = TermC.parse thy "(-#5)\<up>#3"; |
338 > val (SOME ct) = TermC.parse thy "(-#5)\<up>#3"; |