src/HOL/Datatype_Benchmark/ROOT.ML
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 45860 93eda35a8377
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
wenzelm@45860
     1
(*  Title:      HOL/Datatype_Benchmark/ROOT.ML
berghofe@7013
     2
wenzelm@15661
     3
Some rather large datatype examples (from John Harrison).
berghofe@7013
     4
*)
berghofe@7013
     5
wenzelm@44639
     6
Toplevel.timing := true;
wenzelm@7373
     7
wenzelm@45860
     8
use_thys ["Brackin", "Instructions", "SML", "Verilog"];