# HG changeset patch
# User wenzelm
# Date 973547356 -3600
# Node ID 5e82d6cafb5fd8a0e49f38d3c1d141492db60fc9
# Parent  58bb50f694970038118fe3b0ef665b54f4ebb383
inductive_atomize, inductive_rulify;

diff -r 58bb50f69497 -r 5e82d6cafb5f src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Mon Nov 06 22:48:42 2000 +0100
+++ b/src/HOL/Inductive.thy	Mon Nov 06 22:49:16 2000 +0100
@@ -1,21 +1,62 @@
 (*  Title:      HOL/Inductive.thy
     ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
 *)
 
 theory Inductive = Gfp + Sum_Type + NatDef
 files
-  "Tools/induct_method.ML"
-  "Tools/inductive_package.ML"
-  "Tools/datatype_aux.ML"
-  "Tools/datatype_prop.ML"
-  "Tools/datatype_rep_proofs.ML"
-  "Tools/datatype_abs_proofs.ML"
-  "Tools/datatype_package.ML"
-  "Tools/primrec_package.ML":
+  ("Tools/induct_method.ML")
+  ("Tools/inductive_package.ML")
+  ("Tools/datatype_aux.ML")
+  ("Tools/datatype_prop.ML")
+  ("Tools/datatype_rep_proofs.ML")
+  ("Tools/datatype_abs_proofs.ML")
+  ("Tools/datatype_package.ML")
+  ("Tools/primrec_package.ML"):
+
+constdefs
+  forall :: "('a => bool) => bool"
+  "forall P == \<forall>x. P x"
+  implies :: "bool => bool => bool"
+  "implies A B == A --> B"
+
+lemma forall_eq: "(!!x. P x) == Trueprop (forall (\<lambda>x. P x))"
+proof
+  assume "!!x. P x"
+  thus "forall (\<lambda>x. P x)" by (unfold forall_def) blast
+next
+  fix x
+  assume "forall (\<lambda>x. P x)"
+  thus "P x" by (unfold forall_def) blast
+qed
 
+lemma implies_eq: "(A ==> B) == Trueprop (implies A B)"
+proof
+  assume "A ==> B"
+  thus "implies A B" by (unfold implies_def) blast
+next
+  assume "implies A B" and A
+  thus B by (unfold implies_def) blast
+qed
+
+lemmas inductive_atomize = forall_eq implies_eq
+lemmas inductive_rulify = inductive_atomize [symmetric, standard]
+hide const forall implies
+
+use "Tools/induct_method.ML"
 setup InductMethod.setup
+
+use "Tools/inductive_package.ML"
 setup InductivePackage.setup
+
+use "Tools/datatype_aux.ML"
+use "Tools/datatype_prop.ML"
+use "Tools/datatype_rep_proofs.ML"
+use "Tools/datatype_abs_proofs.ML"
+use "Tools/datatype_package.ML"
 setup DatatypePackage.setup
+
+use "Tools/primrec_package.ML"
 setup PrimrecPackage.setup
 
 theorems basic_monos [mono] =