(* equations and functions; functions NOT as lambda-terms

    author: Walther Neuper 2005, 2006

    (c) due to copyright terms

 remove_thy"Equation";

 use_thy"Knowledge/Equation";

 use_thy_only"Knowledge/Equation";

 remove_thy"Equation";

 use_thy"Knowledge/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