# HG changeset patch
# User berghofe
# Date 1037197517 -3600
# Node ID 934d6c1421f20cca56ddc10f29a642c93ce36c35
# Parent  854501b1e957fc997791ea456746718543bf2ce2
Added InductiveRealizer package.

diff -r 854501b1e957 -r 934d6c1421f2 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed Nov 13 15:24:42 2002 +0100
+++ b/src/HOL/Inductive.thy	Wed Nov 13 15:25:17 2002 +0100
@@ -9,6 +9,7 @@
 theory Inductive = Gfp + Sum_Type + Relation + Record
 files
   ("Tools/inductive_package.ML")
+  ("Tools/inductive_realizer.ML")
   ("Tools/inductive_codegen.ML")
   ("Tools/datatype_aux.ML")
   ("Tools/datatype_prop.ML")
@@ -87,6 +88,9 @@
 use "Tools/datatype_codegen.ML"
 setup DatatypeCodegen.setup
 
+use "Tools/inductive_realizer.ML"
+setup InductiveRealizer.setup
+
 use "Tools/inductive_codegen.ML"
 setup InductiveCodegen.setup