src/Tools/isac/Build_Isac.thy
changeset 60763 2121f1a39a64
parent 60762 f10bbfb2b3bb
child 60767 466f0a5bfb73
     1.1 --- a/src/Tools/isac/Build_Isac.thy	Sun Oct 29 07:14:14 2023 +0100
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Thu Nov 16 08:15:46 2023 +0100
     1.3 @@ -169,7 +169,7 @@
     1.4  (** )
     1.5  ( **)
     1.6  \<close> ML \<open>
     1.7 -
     1.8 +@{term Gleichungen}
     1.9  \<close> ML \<open>
    1.10  \<close> 
    1.11  subsection \<open>make Minisubpbl independent from Thy_Info\<close>
    1.12 @@ -181,10 +181,9 @@
    1.13    As next step we go bottom up from Thy_Info.get_theory and remove it.
    1.14    Afterwards $ISABELLE_ISAC_TEST will be changed accordingly.
    1.15  \<close>
    1.16 -(**) (* evaluated in Test_Isac/_Short *)
    1.17 +(** ) (* evaluated in Test_Isac/_Short *)
    1.18    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/000-comments.sml"
    1.19 -(*ML_file "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml" (*still in Test_Theory*)*)
    1.20 -  ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100-init-rootpbl.sml"
    1.21 +  ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml"
    1.22    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml"
    1.23    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150-add-given-Equation.sml"
    1.24    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml"
    1.25 @@ -208,6 +207,7 @@
    1.26    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/800-append-on-Frm.sml"
    1.27  (**)                                          
    1.28    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Specify/i-model.sml"
    1.29 +(**)                                          
    1.30    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Specify/pre-conditions.sml"
    1.31  
    1.32    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/e-collect.sml"
    1.33 @@ -216,7 +216,7 @@
    1.34    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/preliminary.sml"
    1.35    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/calculation.sml"
    1.36    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/vscode-example.sml"
    1.37 -(**)                                          
    1.38 +( **)                                          
    1.39  
    1.40  (* evaluated in Test_Isac/_Short *)                               
    1.41  
    1.42 @@ -275,7 +275,7 @@
    1.43  \<close> ML \<open>
    1.44  
    1.45  \<close> ML \<open>
    1.46 -I_Model.TEST_to_OLD ;
    1.47 +I_Model.TEST_to_OLD  ;
    1.48  I_Model.OLD_to_TEST
    1.49  (*OLD*)
    1.50  (*---*)
    1.51 @@ -283,3 +283,10 @@
    1.52  \<close> ML \<open>
    1.53  \<close>
    1.54  end
    1.55 +
    1.56 +
    1.57 +
    1.58 +
    1.59 +
    1.60 +
    1.61 +