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