# HG changeset patch
# User wenzelm
# Date 1004133638 -7200
# Node ID 5818c5abb415ebcc398edab4ced8a16bbe8461fd
# Parent  3d1780208bf3c91aa98fff0bff70145627eefa33
moved product cases/induct to theory Datatype;

diff -r 3d1780208bf3 -r 5818c5abb415 src/HOL/PreList.thy
--- a/src/HOL/PreList.thy	Sat Oct 27 00:00:05 2001 +0200
+++ b/src/HOL/PreList.thy	Sat Oct 27 00:00:38 2001 +0200
@@ -11,72 +11,9 @@
   Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
   Relation_Power + Calculation + SVC_Oracle:
 
-(*belongs to theory Datatype*)
-declare case_split [cases type: bool]
-
 (*belongs to theory Wellfounded_Recursion*)
 declare wf_induct [induct set: wf]
 
-(*belongs to theory Datatype_Universe; hides popular names *)
-hide const Node Atom Leaf Numb Lim Funs Split Case
-hide type node item
-
-(*belongs to theory Datatype; canonical case/induct rules for 3-7 tuples*)
-lemma prod_cases3 [cases type]: "(!!a b c. y = (a, b, c) ==> P) ==> P"
-  apply (cases y)
-  apply (case_tac b)
-  apply blast
-  done
-
-lemma prod_induct3 [induct type]: "(!!a b c. P (a, b, c)) ==> P x"
-  apply (cases x)
-  apply blast
-  done
-
-lemma prod_cases4 [cases type]: "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
-  apply (cases y)
-  apply (case_tac c)
-  apply blast
-  done
-
-lemma prod_induct4 [induct type]: "(!!a b c d. P (a, b, c, d)) ==> P x"
-  apply (cases x)
-  apply blast
-  done
-
-lemma prod_cases5 [cases type]: "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
-  apply (cases y)
-  apply (case_tac d)
-  apply blast
-  done
-
-lemma prod_induct5 [induct type]: "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
-  apply (cases x)
-  apply blast
-  done
-
-lemma prod_cases6 [cases type]: "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
-  apply (cases y)
-  apply (case_tac e)
-  apply blast
-  done
-
-lemma prod_induct6 [induct type]: "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
-  apply (cases x)
-  apply blast
-  done
-
-lemma prod_cases7 [cases type]: "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
-  apply (cases y)
-  apply (case_tac f)
-  apply blast
-  done
-
-lemma prod_induct7 [induct type]: "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
-  apply (cases x)
-  apply blast
-  done
-
 
 (* generic summation indexed over nat *)