# HG changeset patch
# User wenzelm
# Date 1002135785 -7200
# Node ID a68f930bafb2d32c200995694d49ea227412d6a3
# Parent  4200394242c5a19e95ac2a8a08052144f8df1364
Tools/induct_attrib.ML now part of Pure;

diff -r 4200394242c5 -r a68f930bafb2 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Oct 03 21:01:53 2001 +0200
+++ b/src/HOL/IsaMakefile	Wed Oct 03 21:03:05 2001 +0200
@@ -98,7 +98,7 @@
   SetInterval.thy String.thy Sum_Type.ML Sum_Type.thy \
   Tools/basic_codegen.ML Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
   Tools/datatype_package.ML Tools/datatype_prop.ML \
-  Tools/datatype_rep_proofs.ML Tools/induct_attrib.ML Tools/induct_method.ML \
+  Tools/datatype_rep_proofs.ML Tools/induct_method.ML \
   Tools/inductive_package.ML Tools/inductive_codegen.ML Tools/meson.ML Tools/numeral_syntax.ML \
   Tools/primrec_package.ML Tools/recdef_package.ML \
   Tools/record_package.ML Tools/split_rule.ML \
diff -r 4200394242c5 -r a68f930bafb2 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Wed Oct 03 21:01:53 2001 +0200
+++ b/src/HOL/Typedef.thy	Wed Oct 03 21:03:05 2001 +0200
@@ -6,8 +6,7 @@
 *)
 
 theory Typedef = Set
-files "subset.ML" "equalities.ML" "mono.ML"
-  "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"):
+files "subset.ML" "equalities.ML" "mono.ML" ("Tools/typedef_package.ML"):
 
 (* Courtesy of Stephan Merz *)
 lemma Least_mono: 
@@ -128,7 +127,6 @@
   ultimately show "P x" by (simp only:)
 qed
 
-setup InductAttrib.setup
 use "Tools/typedef_package.ML"
 
 end