# HG changeset patch
# User nipkow
# Date 764362495 -3600
# Node ID 43e36c15a831e117d4455b53576b76507eeacb44
# Parent  38e2eaa2219ffa8953c7289b46ad199a7425e8f1
new field "simps" added

diff -r 38e2eaa2219f -r 43e36c15a831 Datatype.ML
--- a/Datatype.ML	Tue Mar 22 18:07:45 1994 +0100
+++ b/Datatype.ML	Tue Mar 22 19:54:55 1994 +0100
@@ -11,6 +11,7 @@
    val inject : thm list
    val ineq : thm list 
    val cases : thm list
+   val simps : thm list
    val induct_tac : string -> int -> tactic
 end;
 
@@ -480,6 +481,8 @@
 
 val cases = getaxioms rules_case thy;
 
+val simps = inject @ ineq @ cases;
+
 fun induct_tac a = res_inst_tac [(datatype_id,a)] induct;
 
 (* -------------------------------------------------------------------  *)