src/Tools/Code_Generator.thy
changeset 30973 304ab57afa6e
parent 30929 d9343c0aac11
child 31036 64ff53fc0c0c
equal deleted inserted replaced
30972:5b65835ccc92 30973:304ab57afa6e
     6 
     6 
     7 theory Code_Generator
     7 theory Code_Generator
     8 imports Pure
     8 imports Pure
     9 uses
     9 uses
    10   "~~/src/Tools/value.ML"
    10   "~~/src/Tools/value.ML"
       
    11   "~~/src/Tools/quickcheck.ML"
    11   "~~/src/Tools/code/code_name.ML"
    12   "~~/src/Tools/code/code_name.ML"
    12   "~~/src/Tools/code/code_wellsorted.ML" 
    13   "~~/src/Tools/code/code_wellsorted.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"
    15   "~~/src/Tools/code/code_target.ML"
    16   "~~/src/Tools/code/code_target.ML"