1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,37 @@
     1.4 +(* Algebra Einf"uhrung, Unterrichtsversuch IMST-Projekt
     1.5 +   author: Walther Neuper 2007
     1.6 +   (c) due to copyright terms
     1.7 +
     1.8 +remove_thy"AlgEin";
     1.9 +use_thy"Knowledge/AlgEin";
    1.10 +use_thy_only"Knowledge/AlgEin";
    1.11 +
    1.12 +remove_thy"AlgEin";
    1.13 +use_thy"Knowledge/Isac";
    1.14 +*)
    1.15 +
    1.16 +AlgEin = Rational +
    1.17 +(*Poly + ..shouldbe sufficient, but norm_Poly *)
    1.18 +
    1.19 +consts
    1.20 +
    1.21 +  (*new Descriptions in the related problems*)
    1.22 +  KantenUnten     :: bool list => una
    1.23 +  KantenSenkrecht :: bool list => una
    1.24 +  KantenOben      :: bool list => una
    1.25 +  KantenLaenge    :: bool => una
    1.26 +  Querschnitt     :: bool => una
    1.27 +  GesamtLaenge    :: real => una
    1.28 +
    1.29 +  (*Script-names*)
    1.30 +  RechnenSymbolScript :: "[bool,bool,bool list,bool list,bool list,real,
    1.31 +				bool] => bool"
    1.32 +	      ("((Script RechnenSymbolScript (_ _ _ _ _ _ =))// (_))" 9)
    1.33 +
    1.34 +(*
    1.35 +rules
    1.36 +  (*this axiom creates a contradictory formal system,
    1.37 +    see problem TOOODO *)
    1.38 +*)
    1.39 +
    1.40 +end