src/Tools/Code_Generator.thy
changeset 33820 082d9bc6992d
parent 33561 ab01b72715ef
child 33889 4328de748fb2
equal deleted inserted replaced
33816:e08c9f755fca 33820:082d9bc6992d
     3 *)
     3 *)
     4 
     4 
     5 header {* Loading the code generator modules *}
     5 header {* Loading the code generator modules *}
     6 
     6 
     7 theory Code_Generator
     7 theory Code_Generator
     8 imports Auto_Counterexample
     8 imports Pure
     9 uses
     9 uses
       
    10   "~~/src/Tools/auto_counterexample.ML"
    10   "~~/src/Tools/value.ML"
    11   "~~/src/Tools/value.ML"
    11   "~~/src/Tools/quickcheck.ML"
    12   "~~/src/Tools/quickcheck.ML"
    12   "~~/src/Tools/Code/code_preproc.ML" 
    13   "~~/src/Tools/Code/code_preproc.ML" 
    13   "~~/src/Tools/Code/code_thingol.ML"
    14   "~~/src/Tools/Code/code_thingol.ML"
    14   "~~/src/Tools/Code/code_printer.ML"
    15   "~~/src/Tools/Code/code_printer.ML"