diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Knowledge/Simplify.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/Knowledge/Simplify.ML	Wed Aug 25 16:20:07 2010 +0200
@@ -0,0 +1,76 @@
+(* simplification of terms
+   author: Walther Neuper 050912
+   (c) due to copyright terms
+
+use"Knowledge/Simplify.ML";
+use"Simplify.ML";
+*)
+
+
+(** interface isabelle -- isac **)
+
+theory' := overwritel (!theory', [("Simplify.thy",Simplify.thy)]);
+
+(** problems **)
+
+store_pbt
+ (prep_pbt Simplify.thy "pbl_simp" [] e_pblID
+ (["simplification"],
+  [("#Given" ,["term t_"]),
+   ("#Find"  ,["normalform n_"])
+  ],
+  append_rls "e_rls" e_rls [(*for preds in where_*)], 
+  SOME "Simplify t_", 
+  []));
+
+store_pbt
+ (prep_pbt Simplify.thy "pbl_vereinfache" [] e_pblID
+ (["vereinfachen"],
+  [("#Given" ,["term t_"]),
+   ("#Find"  ,["normalform n_"])
+  ],
+  append_rls "e_rls" e_rls [(*for preds in where_*)], 
+  SOME "Vereinfache t_", 
+  []));
+
+(** methods **)
+
+store_met
+    (prep_met Simplify.thy "met_simp" [] e_metID
+	      (["simplification"],
+	       [("#Given" ,["term t_"]),
+		("#Find"  ,["normalform n_"])
+		],
+	       {rew_ord'="tless_true",
+		rls'= e_rls, 
+		calc = [], 
+		srls = e_rls, 
+		prls=e_rls,
+		crls = e_rls, nrls = e_rls},
+	       "empty_script"
+	       ));
+
+(** CAS-command **)
+
+(*.function for handling the cas-input "Simplify (2*a + 3*a)":
+   make a model which is already in ptree-internal format.*)
+(* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
+   val (h,argl) = strip_comb ((term_of o the o (parse thy)) 
+				  "Simplify (2*a + 3*a)");
+   *)
+fun argl2dtss t =
+    [((term_of o the o (parse thy)) "term", t),
+     ((term_of o the o (parse thy)) "normalform", 
+      [(term_of o the o (parse thy)) "N"])
+     ]
+  | argl2dtss _ = raise error "Simplify.ML: wrong argument for argl2dtss";
+
+castab := 
+overwritel (!castab, 
+	    [((term_of o the o (parse thy)) "Simplify",  
+	      (("Isac.thy", ["simplification"], ["no_met"]), 
+	       argl2dtss)),
+	     ((term_of o the o (parse thy)) "Vereinfache",  
+	      (("Isac.thy", ["vereinfachen"], ["no_met"]), 
+	       argl2dtss))
+	     ]);