diff -r 5100a9c3abf8 -r 875b6efa7ced src/Pure/isac/IsacKnowledge/Equation.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/isac/IsacKnowledge/Equation.thy	Wed Jul 21 13:53:39 2010 +0200
@@ -0,0 +1,29 @@
+(* equations and functions; functions NOT as lambda-terms
+   author: Walther Neuper 2005, 2006
+   (c) due to copyright terms
+
+remove_thy"Equation";
+use_thy"IsacKnowledge/Equation";
+use_thy_only"IsacKnowledge/Equation";
+
+remove_thy"Equation";
+use_thy"IsacKnowledge/Isac";
+*)
+
+Equation = Atools +
+
+consts
+
+  (*descriptions in the related problems TODOshift here from Descriptions.thy*)
+  substitution :: bool => una
+
+  (*the CAS-commands*)
+  solve     :: "[bool * 'a] => bool list" (* solve (x+1=2, x) *)
+  solveTest :: "[bool * 'a] => bool list" (* for test collection *)
+  
+  (*Script-names*)
+  Function2Equality  :: "[bool, bool,       bool] \
+					\=> bool"
+                  ("((Script Function2Equality (_ _ =))// (_))" 9)
+
+end
\ No newline at end of file