(* Title:  "MathEngBasic/MathEngBasic.thy"

    Author: Walther Neuper 110226

    (c) due to copyright terms

 Definitions required for both, for Specify and for the Lucas-Interpreter.

 Note (compare \<^ML>\<open>@{theory Know_Store}\<close> cf.03dea0a179d0):

 The files ("xxxxx-def.sml") contain definitions required for ML_structure\<open>Ctree\<close>;

 they also include minimal code required for other "xxxxx-def.sml" files.

 These files have companion files "xxxxx.sml" with all further code,

 located at appropriate positions in the file structure.

 The separation of "xxxxx-def.sml" from "xxxxx.sml" should be overcome by

 appropriate use of polymorphic high order functions.

 *)

 theory MathEngBasic

   imports "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"

   keywords "problem" "method" :: thy_decl

     and "Author" "Theory_Ref" "Problem_Ref" "Method_Ref" 

     "CAS" "Program" "Given" "Where" "Find" "Relate"

 begin

   ML_file thmC.sml

   ML_file "model-def.sml"

   ML_file problem.sml

   ML_file method.sml

   ML_file rewrite.sml

   ML_file "istate-def.sml"

   ML_file "calc-tree-elem.sml"

   ML_file "pre-conds-def.sml"

   ML_file tactic.sml                                     

   ML_file applicable.sml

   ML_file position.sml

   ML_file "specification-def.sml"

   ML_file "ctree-basic.sml"

   ML_file "ctree-access.sml"

   ML_file "ctree-navi.sml"

   ML_file ctree.sml

   ML_file references.sml

   ML_file "state-steps.sml"

   ML_file calculation.sml

 ML \<open>

 \<close> ML \<open>

 Rewrite_Ord.function_empty

 \<close> ML \<open>

 \<close>

 end