1.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Mon Dec 16 15:56:20 2019 +0100
1.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Tue Dec 17 16:31:46 2019 +0100
1.3 @@ -11,7 +11,7 @@
1.4 ML_file model.sml
1.5 ML_file mstools.sml
1.6 ML_file "specification-elems.sml"
1.7 - ML_file istate.sml
1.8 + ML_file "istate-def.sml"
1.9 ML_file tactic.sml
1.10 ML_file position.sml
1.11 ML_file "ctree-basic.sml"
1.12 @@ -21,9 +21,32 @@
1.13
1.14 ML \<open>
1.15 \<close> ML \<open>
1.16 +signature XXX_DEF =
1.17 +sig
1.18 + datatype xxx_def = Aaa of string | Bbb of string
1.19 +end
1.20 \<close> ML \<open>
1.21 +structure Xxx_Def: XXX_DEF(**) =
1.22 +struct
1.23 + datatype xxx_def = Aaa of string | Bbb of string
1.24 +end
1.25 \<close> ML \<open>
1.26 +Xxx_Def.Aaa "works"
1.27 \<close> ML \<open>
1.28 \<close> ML \<open>
1.29 +\<close> ML \<open>
1.30 +signature XXX =
1.31 +sig
1.32 + datatype xxx = Aaa of string | Bbb of string
1.33 +end
1.34 +\<close> ML \<open>
1.35 +structure Xxx: XXX(**) =
1.36 +struct
1.37 + open Xxx_Def
1.38 + datatype xxx = datatype xxx_def
1.39 +end
1.40 +\<close> ML \<open>
1.41 +Xxx.Aaa "works"
1.42 +\<close> ML \<open>
1.43 \<close>
1.44 end