1.1 --- a/src/Tools/isac/IsacKnowledge/Simplify.ML	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,76 +0,0 @@
     1.4 -(* simplification of terms
     1.5 -   author: Walther Neuper 050912
     1.6 -   (c) due to copyright terms
     1.7 -
     1.8 -use"IsacKnowledge/Simplify.ML";
     1.9 -use"Simplify.ML";
    1.10 -*)
    1.11 -
    1.12 -
    1.13 -(** interface isabelle -- isac **)
    1.14 -
    1.15 -theory' := overwritel (!theory', [("Simplify.thy",Simplify.thy)]);
    1.16 -
    1.17 -(** problems **)
    1.18 -
    1.19 -store_pbt
    1.20 - (prep_pbt Simplify.thy "pbl_simp" [] e_pblID
    1.21 - (["simplification"],
    1.22 -  [("#Given" ,["term t_"]),
    1.23 -   ("#Find"  ,["normalform n_"])
    1.24 -  ],
    1.25 -  append_rls "e_rls" e_rls [(*for preds in where_*)], 
    1.26 -  SOME "Simplify t_", 
    1.27 -  []));
    1.28 -
    1.29 -store_pbt
    1.30 - (prep_pbt Simplify.thy "pbl_vereinfache" [] e_pblID
    1.31 - (["vereinfachen"],
    1.32 -  [("#Given" ,["term t_"]),
    1.33 -   ("#Find"  ,["normalform n_"])
    1.34 -  ],
    1.35 -  append_rls "e_rls" e_rls [(*for preds in where_*)], 
    1.36 -  SOME "Vereinfache t_", 
    1.37 -  []));
    1.38 -
    1.39 -(** methods **)
    1.40 -
    1.41 -store_met
    1.42 -    (prep_met Simplify.thy "met_simp" [] e_metID
    1.43 -	      (["simplification"],
    1.44 -	       [("#Given" ,["term t_"]),
    1.45 -		("#Find"  ,["normalform n_"])
    1.46 -		],
    1.47 -	       {rew_ord'="tless_true",
    1.48 -		rls'= e_rls, 
    1.49 -		calc = [], 
    1.50 -		srls = e_rls, 
    1.51 -		prls=e_rls,
    1.52 -		crls = e_rls, nrls = e_rls},
    1.53 -	       "empty_script"
    1.54 -	       ));
    1.55 -
    1.56 -(** CAS-command **)
    1.57 -
    1.58 -(*.function for handling the cas-input "Simplify (2*a + 3*a)":
    1.59 -   make a model which is already in ptree-internal format.*)
    1.60 -(* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
    1.61 -   val (h,argl) = strip_comb ((term_of o the o (parse thy)) 
    1.62 -				  "Simplify (2*a + 3*a)");
    1.63 -   *)
    1.64 -fun argl2dtss t =
    1.65 -    [((term_of o the o (parse thy)) "term", t),
    1.66 -     ((term_of o the o (parse thy)) "normalform", 
    1.67 -      [(term_of o the o (parse thy)) "N"])
    1.68 -     ]
    1.69 -  | argl2dtss _ = raise error "Simplify.ML: wrong argument for argl2dtss";
    1.70 -
    1.71 -castab := 
    1.72 -overwritel (!castab, 
    1.73 -	    [((term_of o the o (parse thy)) "Simplify",  
    1.74 -	      (("Isac.thy", ["simplification"], ["no_met"]), 
    1.75 -	       argl2dtss)),
    1.76 -	     ((term_of o the o (parse thy)) "Vereinfache",  
    1.77 -	      (("Isac.thy", ["vereinfachen"], ["no_met"]), 
    1.78 -	       argl2dtss))
    1.79 -	     ]);