src/HOL/Induct/ROOT.ML
author wenzelm
Tue, 31 Jul 2007 22:21:20 +0200
changeset 24104 719fbe4fb77f
parent 23746 a455e69c31cc
child 24607 fc06b84acd81
permissions -rw-r--r--
simultaneous use_thys;


(* $Id$ *)

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