equal
deleted
inserted
replaced
18 |
18 |
19 val Const ("RatArith.cancel",_) $ zaehler $ nenner = t; |
19 val Const ("RatArith.cancel",_) $ zaehler $ nenner = t; |
20 ---------------------------------------------------------------------*) |
20 ---------------------------------------------------------------------*) |
21 |
21 |
22 |
22 |
23 (*diese vvv funktionen kommen nach src/Isa99/term.sml -------------*) |
23 (*diese vvv funktionen kommen nach src/Isa99/termC.sml -------------*) |
24 fun term2str t = |
24 fun term2str t = |
25 let fun ato (Const(a,T)) n = |
25 let fun ato (Const(a,T)) n = |
26 "\n"^indent n^"Const ( "^a^")" |
26 "\n"^indent n^"Const ( "^a^")" |
27 | ato (Free (a,T)) n = |
27 | ato (Free (a,T)) n = |
28 "\n"^indent n^"Free ( "^a^", "^")" |
28 "\n"^indent n^"Free ( "^a^", "^")" |
35 | ato (f$t') n = ato f n^ato t' (n+1) |
35 | ato (f$t') n = ato f n^ato t' (n+1) |
36 in "\n-------------"^ato t 0^"\n" end; |
36 in "\n-------------"^ato t 0^"\n" end; |
37 fun free2int (t as Free (s, _)) = (((the o int_of_str) s) |
37 fun free2int (t as Free (s, _)) = (((the o int_of_str) s) |
38 handle _ => raise error ("free2int: "^term2str t)) |
38 handle _ => raise error ("free2int: "^term2str t)) |
39 | free2int t = raise error ("free2int: "^term2str t); |
39 | free2int t = raise error ("free2int: "^term2str t); |
40 (*diese ^^^ funktionen kommen nach src/Isa99/term.sml -------------*) |
40 (*diese ^^^ funktionen kommen nach src/Isa99/termC.sml -------------*) |
41 |
41 |
42 |
42 |
43 (* remark on exceptions: 'error' is implemented by Isabelle |
43 (* remark on exceptions: 'error' is implemented by Isabelle |
44 as the typical system error *) |
44 as the typical system error *) |
45 |
45 |