src/Tools/isac/Build_Isac.thy
changeset 59773 d88bb023c380
parent 59687 62edafdc1df5
child 59777 23c143ffb22f
     1.1 --- a/src/Tools/isac/Build_Isac.thy	Fri Jan 17 12:37:21 2020 +0100
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Fri Jan 17 13:14:11 2020 +0100
     1.3 @@ -25,6 +25,7 @@
     1.4  
     1.5  (*    theory Calculate imports "~~/src/Tools/isac/CalcElements/CalcElements"
     1.6          ML_file calculate.sml
     1.7 +
     1.8        theory ListC imports "~~/src/Tools/isac/CalcElements/CalcElements"
     1.9      theory Prog_Expr imports Calculate ListC
    1.10        theory Program imports "~~/src/Tools/isac/CalcElements/CalcElements"
    1.11 @@ -102,7 +103,7 @@
    1.12  #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
    1.13  \<close> ML \<open>
    1.14  \<close>
    1.15 -ML \<open>Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close>
    1.16 +ML \<open>Num_Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close>
    1.17  ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close>
    1.18  ML \<open>Input_Descript.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close>
    1.19  ML \<open>Math_Engine.me;\<close>