1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/sml/IsacKnowledge/AlgEin.ML	Thu Apr 05 17:50:57 2007 +0200
     1.3 @@ -0,0 +1,84 @@
     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 +use"IsacKnowledge/AlgEin.ML";
     1.9 +use"AlgEin.ML";
    1.10 +
    1.11 +remove_thy"Typefix";
    1.12 +remove_thy"AlgEin";
    1.13 +use_thy"IsacKnowledge/Isac";
    1.14 +*)
    1.15 +
    1.16 +(** interface isabelle -- isac **)
    1.17 +
    1.18 +theory' := overwritel (!theory', [("AlgEin.thy",AlgEin.thy)]);
    1.19 +
    1.20 +(** problems **)
    1.21 +
    1.22 +store_pbt
    1.23 + (prep_pbt AlgEin.thy "pbl_algein" [] e_pblID
    1.24 + (["Berechnung"], [], e_rls, None, 
    1.25 +  []));
    1.26 +(* WN070405
    1.27 +store_pbt
    1.28 + (prep_pbt AlgEin.thy "pbl_algein_num" [] e_pblID
    1.29 + (["numerische", "Berechnung"],
    1.30 +  [("#Given" ,["KantenUnten u_", "KantenSenkrecht s_", "KantenOben o_"]),
    1.31 +   ("#Find"  ,["GesamtLaenge l_"])
    1.32 +  ],
    1.33 +  append_rls "e_rls" e_rls [], 
    1.34 +  None, 
    1.35 +  []));
    1.36 +*)
    1.37 +store_pbt
    1.38 + (prep_pbt AlgEin.thy "pbl_algein_numsym" [] e_pblID
    1.39 + (["numerischSymbolische", "Berechnung"],
    1.40 +  [("#Given" ,["KantenLaenge k_","Querschnitt q_",
    1.41 +	       "KantenUnten u_", "KantenSenkrecht s_", "KantenOben o_"]),
    1.42 +   ("#Find"  ,["GesamtLaenge l_"])
    1.43 +  ],
    1.44 +  e_rls, 
    1.45 +  None, 
    1.46 +  [["Berechnung","erstNumerisch"],["Berechnung","erstSymbolisch"]]));
    1.47 +
    1.48 +(* show_ptyps();
    1.49 +   *)
    1.50 +
    1.51 +
    1.52 +(** methods **)
    1.53 +
    1.54 +store_met
    1.55 +    (prep_met Biegelinie.thy "met_algein" [] e_metID
    1.56 +	      (["Berechnung"],
    1.57 +	       [],
    1.58 +	       {rew_ord'="tless_true", rls'= Erls, calc = [], 
    1.59 +		srls = Erls, prls = Erls,
    1.60 +		crls =Erls , nrls = Erls},
    1.61 +"empty_script"
    1.62 +));
    1.63 +
    1.64 +store_met
    1.65 +    (prep_met Biegelinie.thy "met_algein_numsym" [] e_metID
    1.66 +	      (["Berechnung","erstNumerisch"],
    1.67 +	       [],
    1.68 +	       {rew_ord'="tless_true", rls'= Erls, calc = [], 
    1.69 +		srls = Erls, prls = Erls,
    1.70 +		crls =Erls , nrls = Erls},
    1.71 +"empty_script"
    1.72 +));
    1.73 +
    1.74 +store_met
    1.75 +    (prep_met Biegelinie.thy "met_algein_symnum" [] e_metID
    1.76 +	      (["Berechnung","erstSymbolisch"],
    1.77 +	       [],
    1.78 +	       {rew_ord'="tless_true", rls'= Erls, calc = [], 
    1.79 +		srls = Erls, prls = Erls,
    1.80 +		crls =Erls , nrls = Erls},
    1.81 +"empty_script"
    1.82 +));
    1.83 +
    1.84 +(* show_mets();
    1.85 +   *)
    1.86 +(* use"IsacKnowledge/AlgEin.ML";
    1.87 +   *)
    1.88 \ No newline at end of file

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/sml/IsacKnowledge/AlgEin.thy	Thu Apr 05 17:50:57 2007 +0200
     2.3 @@ -0,0 +1,25 @@
     2.4 +(* Algebra Einf"uhrung, Unterrichtsversuch IMST-Projekt
     2.5 +   author: Walther Neuper 2007
     2.6 +   (c) due to copyright terms
     2.7 +
     2.8 +remove_thy"AlgEin";
     2.9 +use_thy"IsacKnowledge/AlgEin";
    2.10 +use_thy_only"IsacKnowledge/AlgEin";
    2.11 +
    2.12 +remove_thy"AlgEin";
    2.13 +use_thy"IsacKnowledge/Isac";
    2.14 +*)
    2.15 +
    2.16 +AlgEin = Simplify +
    2.17 +
    2.18 +consts
    2.19 +
    2.20 +  (*new Descriptions in the related problems*)
    2.21 +  KantenUnten     :: bool list => una
    2.22 +  KantenSenkrecht :: bool list => una
    2.23 +  KantenOben      :: bool list => una
    2.24 +  KantenLaenge    :: bool => una
    2.25 +  Querschnitt     :: bool => una
    2.26 +  GesamtLaenge    :: real => una
    2.27 +
    2.28 +end