src/Tools/isac/Build_Isac.thy
changeset 60752 77958bc6ed7d
parent 60747 2eff296ab809
child 60753 30eb1f314f5c
     1.1 --- a/src/Tools/isac/Build_Isac.thy	Wed Sep 20 16:51:08 2023 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Sun Sep 24 20:04:41 2023 +0200
     1.3 @@ -181,11 +181,16 @@
     1.4    As next step we go bottom up from Thy_Info.get_theory and remove it.
     1.5    Afterwards $ISABELLE_ISAC_TEST will be changed accordingly.
     1.6  \<close>
     1.7 -(**) (* evaluated in Test_Isac/_Short * )
     1.8 +(**) (* evaluated in Test_Isac/_Short *)
     1.9    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/000-comments.sml"
    1.10    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100-init-rootpbl.sml"
    1.11    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml"
    1.12    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150-add-given-Equation.sml"
    1.13 +ML \<open>
    1.14 +\<close> ML \<open>
    1.15 +
    1.16 +\<close> ML \<open>
    1.17 +\<close> 
    1.18    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml"
    1.19    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method.sml"
    1.20    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method-NEXT_STEP.sml"
    1.21 @@ -216,13 +221,7 @@
    1.22    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/calculation.sml"
    1.23    ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/vscode-example.sml"
    1.24  
    1.25 -( * evaluated in Test_Isac/_Short *)                               
    1.26 -ML \<open>
    1.27 -\<close> ML \<open>
    1.28 -\<close> ML \<open>
    1.29 -\<close> ML \<open>
    1.30 -\<close> ML \<open>
    1.31 -\<close> 
    1.32 +(* evaluated in Test_Isac/_Short *)                               
    1.33  
    1.34  section \<open>check presence of definitions from directories\<close>
    1.35