(* Algebra Einf"uhrung, Unterrichtsversuch IMST-Projekt

    author: Walther Neuper 2007

    (c) due to copyright terms

 remove_thy"AlgEin";

 use_thy"IsacKnowledge/AlgEin";

 use_thy_only"IsacKnowledge/AlgEin";

 remove_thy"AlgEin";

 use_thy"IsacKnowledge/Isac";

 *)

 AlgEin = Rational +

 (*Poly + ..shouldbe sufficient, but norm_Poly *)

 consts

   (*new Descriptions in the related problems*)

   KantenUnten     :: bool list => una

   KantenSenkrecht :: bool list => una

   KantenOben      :: bool list => una

   KantenLaenge    :: bool => una

   Querschnitt     :: bool => una

   GesamtLaenge    :: real => una

   (*Script-names*)

   RechnenSymbolScript :: "[bool,bool,bool list,bool list,bool list,real,

 				bool] => bool"

 	      ("((Script RechnenSymbolScript (_ _ _ _ _ _ =))// (_))" 9)

 (*

 rules

   (*this axiom creates a contradictory formal system,

     see problem TOOODO *)

 *)

 end