src/Tools/isac/Build_Isac.thy
changeset 60567 bb3140a02f3d
parent 60566 04f8699d2c9d
child 60571 19a172de0bb5
equal deleted inserted replaced
60566:04f8699d2c9d 60567:bb3140a02f3d
   107   theory Interpret imports "$ISABELLE_ISAC/Specify/Specify"
   107   theory Interpret imports "$ISABELLE_ISAC/Specify/Specify"
   108   $ISABELLE_ISAC/Interpret
   108   $ISABELLE_ISAC/Interpret
   109     ML_file istate.sml
   109     ML_file istate.sml
   110     ML_file "sub-problem.sml"
   110     ML_file "sub-problem.sml"
   111     ML_file "thy-read.sml"
   111     ML_file "thy-read.sml"
       
   112     ML_file "li-tool.sml"
   112     ML_file "solve-step.sml"
   113     ML_file "solve-step.sml"
   113     ML_file "error-pattern.sml"
   114     ML_file "error-pattern.sml"
   114     ML_file derive.sml
   115     ML_file derive.sml
   115     ML_file "li-tool.sml"
       
   116     ML_file "lucas-interpreter.sml"
   116     ML_file "lucas-interpreter.sml"
   117     ML_file "step-solve.sml"
   117     ML_file "step-solve.sml"
   118 ( ** )    "Interpret/Interpret"( **)
   118 ( ** )    "Interpret/Interpret"( **)
   119 (*
   119 (*
   120   theory MathEngine imports Interpret.Interpret
   120   theory MathEngine imports Interpret.Interpret