1.1 --- a/src/Tools/isac/Build_Isac.thy	Thu Jun 05 17:56:53 2014 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Thu Jun 05 18:10:46 2014 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4    and proceed from the ancestors towards the siblings.
     1.5  *}
     1.6  
     1.7 -text {*check presence of definitions from directories*}
     1.8 +section {*check presence of definitions from directories*}
     1.9  
    1.10  ML {* is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
    1.11  ML {* me; (*from "Interpret/mathengine.sml"*) *}
    1.12 @@ -79,4 +79,39 @@
    1.13  ML {* @{theory "Isac"} *}
    1.14  ML {* ! isab_thm_thy *}
    1.15  
    1.16 +section {* State of approaching Isabelle by Isac *}
    1.17 +text {* 
    1.18 +  Mathias Lehnfeld gives the following list in his thesis in section 
    1.19 +  4.2.3 Relation to Ongoing Isabelle Development.
    1.20 +*}
    1.21 +subsection {* (0) Survey on remaining Unsynchronized.ref *}
    1.22 +subsection {* (1) Exploit parallelism for concurrent session management *}
    1.23 +subsection {* (2) Make Isac’s programming language usable *}
    1.24 +subsection {* (3) Adopt Isabelle’s numeral computation for Isac *}
    1.25 +text {* 
    1.26 +  In 2002 isac already strived for floating point numbers. Since that time
    1.27 +  isac represents numerals as "Free", see below (*1*). These experiments are
    1.28 +  unsatisfactory with respect to logical soundness.
    1.29 +  Since Isabelle now has started to care about floating point numbers, it is high 
    1.30 +  time to adopt these together with the other numerals. Isabelle2012/13's numerals
    1.31 +  are different from Isabelle2011, see "test/Tools/isac/ProgLang/termC.sml".
    1.32 +  
    1.33 +  The transition from "Free" to standard numerals is a task to be scheduled for 
    1.34 +  several weeks. The urgency of this task follows from the experience, 
    1.35 +  that (1.2) for "thehier" is very hard, because "num_str" seems to destroy 
    1.36 +  some of the long identifiers of theorems which would tremendously simplify
    1.37 +  building a hierarchy of theorems according to (1.2), see (*2*) below.
    1.38 +*}
    1.39 +ML {*(*1*) Free ("123.456", HOLogic.realT) *}
    1.40 +ML {*(*2*)
    1.41 +val unknown = filter ((curry op= "??.unknown") o fst) isacrlsthms';
    1.42 +unknown |> nth 1 |> snd |> term_to_string''' @{theory};
    1.43 +unknown |> nth 2 |> snd |> term_to_string''' @{theory};
    1.44 +(*but these seem ok:*)
    1.45 +  Thm.get_name_hint @{thm add_0};
    1.46 +  Thm.get_name_hint (num_str @{thm add_0});
    1.47 +*}
    1.48 +subsection {* (4) Improve the efficiency of Isac’s rewrite-engine *}
    1.49 +subsection {* (5) Adopt Isabelle/jEdit for Isac *}
    1.50 +
    1.51  end