# HG changeset patch
# User berghofe
# Date 1177420722 -7200
# Node ID e5f947e0ade8f59a2333a48b5b3ed72967228913
# Parent  8bc6fbbe1d0ffd84b741cfc2a108c230ac3ec3f2
Added datatype_case.

diff -r 8bc6fbbe1d0f -r e5f947e0ade8 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Tue Apr 24 15:18:09 2007 +0200
+++ b/src/HOL/Inductive.thy	Tue Apr 24 15:18:42 2007 +0200
@@ -18,6 +18,7 @@
   ("Tools/datatype_abs_proofs.ML")
   ("Tools/datatype_realizer.ML")
   ("Tools/datatype_hooks.ML")
+  ("Tools/datatype_case.ML")
   ("Tools/datatype_package.ML")
   ("Tools/datatype_codegen.ML")
   ("Tools/recfun_codegen.ML")
@@ -113,6 +114,7 @@
 use "Tools/datatype_prop.ML"
 use "Tools/datatype_rep_proofs.ML"
 use "Tools/datatype_abs_proofs.ML"
+use "Tools/datatype_case.ML"
 use "Tools/datatype_realizer.ML"
 
 use "Tools/datatype_hooks.ML"