1.1 --- a/src/Tools/isac/KEStore.thy	Thu Mar 15 12:42:04 2018 +0100
     1.2 +++ b/src/Tools/isac/KEStore.thy	Thu Mar 15 12:45:31 2018 +0100
     1.3 @@ -6,31 +6,6 @@
     1.4  imports "~~/src/HOL/Complex_Main"
     1.5  begin
     1.6    ML_file "~~/src/Tools/isac/library.sml"
     1.7 -
     1.8 -
     1.9 -ML {*
    1.10 -*} ML {* (* how declare a recursive datatype *)
    1.11 -*} ML {*
    1.12 -datatype rls = Erls | Rls of {rules: rule list, erls: rls} 
    1.13 -and rule = Rls_ of rls
    1.14 -*} ML {*
    1.15 -*} ML {*
    1.16 -*} ML {*
    1.17 -*}
    1.18 -
    1.19 -
    1.20 -
    1.21 -
    1.22 -
    1.23 -
    1.24 -
    1.25 -
    1.26 -
    1.27 -
    1.28 -
    1.29 -
    1.30 -
    1.31 -
    1.32    ML_file "~~/src/Tools/isac/calcelems.sml"
    1.33  
    1.34  section {* Knowledge elements for problems and methods *}