equal
deleted
inserted
replaced
1 (* Algebra Einf"uhrung, Unterrichtsversuch IMST-Projekt |
|
2 author: Walther Neuper 2007 |
|
3 (c) due to copyright terms |
|
4 |
|
5 remove_thy"AlgEin"; |
|
6 use_thy"IsacKnowledge/AlgEin"; |
|
7 use_thy_only"IsacKnowledge/AlgEin"; |
|
8 |
|
9 remove_thy"AlgEin"; |
|
10 use_thy"IsacKnowledge/Isac"; |
|
11 *) |
|
12 |
|
13 AlgEin = Rational + |
|
14 (*Poly + ..shouldbe sufficient, but norm_Poly *) |
|
15 |
|
16 consts |
|
17 |
|
18 (*new Descriptions in the related problems*) |
|
19 KantenUnten :: bool list => una |
|
20 KantenSenkrecht :: bool list => una |
|
21 KantenOben :: bool list => una |
|
22 KantenLaenge :: bool => una |
|
23 Querschnitt :: bool => una |
|
24 GesamtLaenge :: real => una |
|
25 |
|
26 (*Script-names*) |
|
27 RechnenSymbolScript :: "[bool,bool,bool list,bool list,bool list,real, |
|
28 bool] => bool" |
|
29 ("((Script RechnenSymbolScript (_ _ _ _ _ _ =))// (_))" 9) |
|
30 |
|
31 (* |
|
32 rules |
|
33 (*this axiom creates a contradictory formal system, |
|
34 see problem TOOODO *) |
|
35 *) |
|
36 |
|
37 end |
|