|
1 (* Title: test/Tools/isac/Isac.thy |
|
2 Author: Walther Neuper, TU Graz, 2010 |
|
3 (c) due to copyright terms |
|
4 |
|
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
|
6 10 20 30 40 50 60 70 80 |
|
7 *) |
|
8 |
|
9 "--------------------------------------------------------"; |
|
10 "--------------------------------------------------------"; |
|
11 "table of contents --------------------------------------"; |
|
12 "--------------------------------------------------------"; |
|
13 "-------- fill ! theory' with data ----------------------"; |
|
14 "--------------------------------------------------------"; |
|
15 "--------------------------------------------------------"; |
|
16 "--------------------------------------------------------"; |
|
17 |
|
18 |
|
19 "-------- fill ! theory' with data ----------------------"; |
|
20 "-------- fill ! theory' with data ----------------------"; |
|
21 "-------- fill ! theory' with data ----------------------"; |
|
22 val allthys = theory "Isac"(**@{theory}*) :: |
|
23 Theory.ancestors_of (*@{theory}*) (theory "Isac"); |
|
24 val isabthys = Theory.ancestors_of first_isac_thy; |
|
25 val isacthys = subtract Theory.eq_thy isabthys allthys; |
|
26 "--------------------------------------------------------"; |
|
27 map Context.theory_name allthys; |
|
28 map Context.theory_name isabthys; |
|
29 if map Context.theory_name isacthys = |
|
30 ["Isac", "Test", "AlgEin", "Biegelinie", "DiffApp", "Vect", "PolyMinus", |
|
31 "EqSystem", "Integrate", "Diff", "LogExp", "Trig", "Calculus", "PolyEq", |
|
32 "RootRatEq", "RootRat", "RatEq", "RootEq", "LinEq", "Root", "Equation", |
|
33 "Rational", "Poly", "Simplify", "Atools", "Descript", "Delete", |
|
34 "Language", "Script", "Tools", "ListC"] then () |
|
35 else error "isac.sml: names of isac theories changed"; |
|
36 "--------------------------------------------------------"; |
|
37 val _ = theory' := (map Context.theory_name isacthys) ~~ isacthys; |
|
38 length (! theory'); |
|
39 |
|
40 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
|
41 |
|
42 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |