# HG changeset patch
# User wenzelm
# Date 1014318588 -3600
# Node ID 32292d83367be3b8ed825388b7df69fbcebbd4f2
# Parent  d6a0d168291e4a8fcfe58fbd9e7682c66eef815d
include theory Record (tuned dependencies);

diff -r d6a0d168291e -r 32292d83367b src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Feb 21 20:09:19 2002 +0100
+++ b/src/HOL/Inductive.thy	Thu Feb 21 20:09:48 2002 +0100
@@ -6,7 +6,7 @@
 
 header {* Support for inductive sets and types *}
 
-theory Inductive = Gfp + Sum_Type + Relation
+theory Inductive = Gfp + Sum_Type + Relation + Record
 files
   ("Tools/inductive_package.ML")
   ("Tools/inductive_codegen.ML")