# HG changeset patch
# User berghofe
# Date 1264867189 -3600
# Node ID cca208c8d619b936f773c1b38c4ea902d06a5aef
# Parent  c1e8af37ee7577a8e42db75e7dfc32a64b7549c7
Added setup for simplification of equality constraints in cases rules.

diff -r c1e8af37ee75 -r cca208c8d619 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Jan 30 16:58:46 2010 +0100
+++ b/src/HOL/HOL.thy	Sat Jan 30 16:59:49 2010 +0100
@@ -1453,6 +1453,7 @@
   val atomize = @{thms induct_atomize}
   val rulify = @{thms induct_rulify'}
   val rulify_fallback = @{thms induct_rulify_fallback}
+  val equal_def = @{thm induct_equal_def}
   fun dest_def (Const (@{const_name induct_equal}, _) $ t $ u) = SOME (t, u)
     | dest_def _ = NONE
   val trivial_tac = match_tac @{thms induct_trueI}