src/Tools/isac/Build_Isac.thy
changeset 60317 638d02a9a96a
parent 60217 1d9fee958a46
child 60428 203438ff792f
     1.1 --- a/src/Tools/isac/Build_Isac.thy	Fri May 07 18:12:51 2021 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Tue Jun 01 15:41:23 2021 +0200
     1.3 @@ -41,27 +41,23 @@
     1.4      ML_file contextC.sml
     1.5      ML_file environment.sml
     1.6  ( ** )    "BaseDefinitions/BaseDefinitions"( **)
     1.7 -
     1.8 -(*    theory Calculate imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
     1.9 -      $ISABELLE_ISAC/ProgLang
    1.10 +(*
    1.11 +      theory Calculate imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    1.12 +        at $ISABELLE_ISAC/ProgLang
    1.13          ML_file evaluate.sml
    1.14 -
    1.15        theory ListC imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    1.16 -      $ISABELLE_ISAC/ProgLang
    1.17 -    theory Prog_Expr imports Calculate ListC
    1.18 -    $ISABELLE_ISAC/ProgLang
    1.19        theory Program imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    1.20 -      theory Prog_Tac imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    1.21 +    theory Prog_Expr imports Calculate ListC Program
    1.22 +     theory Prog_Tac imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    1.23        theory Tactical imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
    1.24 -    theory Auto_Prog imports Program Prog_Tac Tactical begin
    1.25 -    $ISABELLE_ISAC/ProgLang
    1.26 +    theory Auto_Prog imports Prog_Tac Tactical
    1.27    theory ProgLang imports Prog_Expr Auto_Prog
    1.28 -  $ISABELLE_ISAC/ProgLang
    1.29 +    at $ISABELLE_ISAC/ProgLang
    1.30  ( ** )    "ProgLang/ProgLang"( **)
    1.31  (*
    1.32    theory MathEngBasic imports
    1.33      "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"
    1.34 -  $ISABELLE_ISAC/MathEngBasic
    1.35 +    at $ISABELLE_ISAC/MathEngBasic
    1.36      ML_file thmC.sml
    1.37      ML_file problem.sml
    1.38      ML_file method.sml