equal
deleted
inserted
replaced
7 |
7 |
8 OR tty (unusable: after errors wrong toplevel): |
8 OR tty (unusable: after errors wrong toplevel): |
9 $ cd "/home/neuper/proto2/isac/src/sml" |
9 $ cd "/home/neuper/proto2/isac/src/sml" |
10 $ isabelle-process HOL HOL-Isac |
10 $ isabelle-process HOL HOL-Isac |
11 ML> use_thy "Isac_Mathengine"; |
11 ML> use_thy "Isac_Mathengine"; |
|
12 |
|
13 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
|
14 10 20 30 40 50 60 70 80 |
12 *) |
15 *) |
13 |
16 |
14 header {* Loading the isac mathengine *} |
17 header {* Loading the isac mathengine *} |
15 |
18 |
16 theory Isac_Mathengine |
19 theory Isac_Mathengine |
28 use "Scripts/calculate.sml" |
31 use "Scripts/calculate.sml" |
29 use "Scripts/rewrite.sml" |
32 use "Scripts/rewrite.sml" |
30 use_thy"Scripts/Script" |
33 use_thy"Scripts/Script" |
31 use "Scripts/scrtools.sml" |
34 use "Scripts/scrtools.sml" |
32 |
35 |
|
36 ML {* |
|
37 member; |
|
38 @{term 111}; |
|
39 *} |
|
40 |
33 use "ME/mstools.sml" |
41 use "ME/mstools.sml" |
|
42 |
|
43 |
34 |
44 |
35 |
45 |
36 (* |
46 (* |
37 use "ME/ctree.sml" |
47 use "ME/ctree.sml" |
38 use "ME/ptyps.sml" |
48 use "ME/ptyps.sml" |