src/Tools/Code_Generator.thy
changeset 31036 64ff53fc0c0c
parent 30973 304ab57afa6e
child 31125 80218ee73167
equal deleted inserted replaced
31035:de0a20a030fd 31036:64ff53fc0c0c
     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/quickcheck.ML"
    12   "~~/src/Tools/code/code_name.ML"
       
    13   "~~/src/Tools/code/code_wellsorted.ML" 
    12   "~~/src/Tools/code/code_wellsorted.ML" 
    14   "~~/src/Tools/code/code_thingol.ML"
    13   "~~/src/Tools/code/code_thingol.ML"
    15   "~~/src/Tools/code/code_printer.ML"
    14   "~~/src/Tools/code/code_printer.ML"
    16   "~~/src/Tools/code/code_target.ML"
    15   "~~/src/Tools/code/code_target.ML"
    17   "~~/src/Tools/code/code_ml.ML"
    16   "~~/src/Tools/code/code_ml.ML"