src/HOL/Induct/ROOT.ML
author huffman
Fri, 28 Oct 2011 11:02:27 +0200
changeset 45284 ae78a4ffa81d
parent 39616 8052101883c3
permissions -rw-r--r--
use simproc_setup for cancellation simprocs, to get proper name bindings

Unsynchronized.setmp quick_and_dirty true
  use_thys ["Common_Patterns"];

use_thys ["QuoDataType", "QuoNestedDataType", "Term", "SList",
  "ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", "Com"];