1.1 --- a/src/Tools/isac/IsacKnowledge/AlgEin.thy	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,37 +0,0 @@
     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"IsacKnowledge/AlgEin";
    1.10 -use_thy_only"IsacKnowledge/AlgEin";
    1.11 -
    1.12 -remove_thy"AlgEin";
    1.13 -use_thy"IsacKnowledge/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