# HG changeset patch
# User wenzelm
# Date 1003431599 -7200
# Node ID ef7d619e2c88a59833046fc06980d0a2e0aea9fc
# Parent  f4c1882dde2c4d5e2e6bc2167037b3f164e2b23f
moved InductMethod.setup to theory HOL;

diff -r f4c1882dde2c -r ef7d619e2c88 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Oct 18 20:59:33 2001 +0200
+++ b/src/HOL/Inductive.thy	Thu Oct 18 20:59:59 2001 +0200
@@ -17,63 +17,6 @@
   ("Tools/primrec_package.ML"):
 
 
-subsection {* Proof by cases and induction *}
-
-text {* Proper handling of non-atomic rule statements. *}
-
-constdefs
-  forall :: "('a => bool) => bool"
-  "forall P == \<forall>x. P x"
-  implies :: "bool => bool => bool"
-  "implies A B == A --> B"
-  equal :: "'a => 'a => bool"
-  "equal x y == x = y"
-  conj :: "bool => bool => bool"
-  "conj A B == A & B"
-
-lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
-  by (simp only: atomize_all forall_def)
-
-lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
-  by (simp only: atomize_imp implies_def)
-
-lemma equal_eq: "(x == y) == Trueprop (equal x y)"
-  by (simp only: atomize_eq equal_def)
-
-lemma forall_conj: "forall (\<lambda>x. conj (A x) (B x)) = conj (forall A) (forall B)"
-  by (unfold forall_def conj_def) blast
-
-lemma implies_conj: "implies C (conj A B) = conj (implies C A) (implies C B)"
-  by (unfold implies_def conj_def) blast
-
-lemma conj_curry: "(conj A B ==> C) == (A ==> B ==> C)"
-  by (simp only: atomize_imp atomize_eq conj_def) (rule equal_intr_rule, blast+)
-
-lemmas inductive_atomize = forall_eq implies_eq equal_eq
-lemmas inductive_rulify1 = inductive_atomize [symmetric, standard]
-lemmas inductive_rulify2 = forall_def implies_def equal_def conj_def
-lemmas inductive_conj = forall_conj implies_conj conj_curry
-
-hide const forall implies equal conj
-
-
-text {* Method setup. *}
-
-ML {*
-  structure InductMethod = InductMethodFun
-  (struct
-    val dest_concls = HOLogic.dest_concls;
-    val cases_default = thm "case_split";
-    val conjI = thm "conjI";
-    val atomize = thms "inductive_atomize";
-    val rulify1 = thms "inductive_rulify1";
-    val rulify2 = thms "inductive_rulify2";
-  end);
-*}
-
-setup InductMethod.setup
-
-
 subsection {* Inductive sets *}
 
 text {* Inversion of injective functions. *}
@@ -124,6 +67,8 @@
 
 subsubsection {* Inductive datatypes and primitive recursion *}
 
+text {* Package setup. *}
+
 use "Tools/datatype_aux.ML"
 use "Tools/datatype_prop.ML"
 use "Tools/datatype_rep_proofs.ML"