neuper@37871: (* Algebra Einf"uhrung, Unterrichtsversuch IMST-Projekt
neuper@37871:    author: Walther Neuper 2007
neuper@37871:    (c) due to copyright terms
neuper@37871: 
neuper@37871: remove_thy"AlgEin";
neuper@37871: use_thy"IsacKnowledge/AlgEin";
neuper@37871: use_thy_only"IsacKnowledge/AlgEin";
neuper@37871: 
neuper@37871: remove_thy"AlgEin";
neuper@37871: use_thy"IsacKnowledge/Isac";
neuper@37871: *)
neuper@37871: 
neuper@37871: AlgEin = Rational +
neuper@37871: (*Poly + ..shouldbe sufficient, but norm_Poly *)
neuper@37871: 
neuper@37871: consts
neuper@37871: 
neuper@37871:   (*new Descriptions in the related problems*)
neuper@37871:   KantenUnten     :: bool list => una
neuper@37871:   KantenSenkrecht :: bool list => una
neuper@37871:   KantenOben      :: bool list => una
neuper@37871:   KantenLaenge    :: bool => una
neuper@37871:   Querschnitt     :: bool => una
neuper@37871:   GesamtLaenge    :: real => una
neuper@37871: 
neuper@37871:   (*Script-names*)
neuper@37871:   RechnenSymbolScript :: "[bool,bool,bool list,bool list,bool list,real,
neuper@37871: 				bool] => bool"
neuper@37871: 	      ("((Script RechnenSymbolScript (_ _ _ _ _ _ =))// (_))" 9)
neuper@37871: 
neuper@37871: (*
neuper@37871: rules
neuper@37871:   (*this axiom creates a contradictory formal system,
neuper@37871:     see problem TOOODO *)
neuper@37871: *)
neuper@37871: 
neuper@37871: end