src/HOL/SMT/SMT_Base.thy
changeset 36891 e0d295cb8bfd
parent 36884 88cf4896b980
child 36893 48cf03469dc6
equal deleted inserted replaced
36890:0ab4217a07b1 36891:e0d295cb8bfd
     6 
     6 
     7 theory SMT_Base
     7 theory SMT_Base
     8 imports Real "~~/src/HOL/Word/Word"
     8 imports Real "~~/src/HOL/Word/Word"
     9 uses
     9 uses
    10   "~~/src/Tools/cache_io.ML"
    10   "~~/src/Tools/cache_io.ML"
       
    11   ("Tools/smt_additional_facts.ML")
    11   ("Tools/smt_normalize.ML")
    12   ("Tools/smt_normalize.ML")
    12   ("Tools/smt_monomorph.ML")
    13   ("Tools/smt_monomorph.ML")
    13   ("Tools/smt_translate.ML")
    14   ("Tools/smt_translate.ML")
    14   ("Tools/smt_solver.ML")
    15   ("Tools/smt_solver.ML")
    15   ("Tools/smtlib_interface.ML")
    16   ("Tools/smtlib_interface.ML")
   128 
   129 
   129 
   130 
   130 
   131 
   131 section {* Setup *}
   132 section {* Setup *}
   132 
   133 
       
   134 use "Tools/smt_additional_facts.ML"
   133 use "Tools/smt_normalize.ML"
   135 use "Tools/smt_normalize.ML"
   134 use "Tools/smt_monomorph.ML"
   136 use "Tools/smt_monomorph.ML"
   135 use "Tools/smt_translate.ML"
   137 use "Tools/smt_translate.ML"
   136 use "Tools/smt_solver.ML"
   138 use "Tools/smt_solver.ML"
   137 use "Tools/smtlib_interface.ML"
   139 use "Tools/smtlib_interface.ML"