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