(* Title:  "MathEngBasic/MathEngBasic.thy"

   Author: Walther Neuper 110226

   (c) due to copyright terms

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

*)

theory MathEngBasic

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

  keywords "method" :: thy_decl

    and "Author" "Program" "Given" "Where" "Find" "Relate"

begin

  ML_file thmC.sml

  ML_file problem.sml

  ML_file method.sml

  ML_file rewrite.sml

  ML_file "model-def.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>                                

\<close> ML \<open>

\<close>

end