src/HOL/Codegenerator_Test/ROOT.ML
author wenzelm
Wed, 25 Aug 2010 18:38:49 +0200
changeset 38716 3c3b4ad683d5
parent 37708 694815d76240
child 48624 9b71daba4ec7
permissions -rw-r--r--
approximation_oracle: actually match true/false in ML, not arbitrary values;

use_thys ["Generate", "Generate_Pretty"];