# HG changeset patch
# User wenzelm
# Date 1002135713 -7200
# Node ID 4200394242c5a19e95ac2a8a08052144f8df1364
# Parent  03c4a5c08a79cfded45c1d6d576f87be2137e97c
Isar/induct_attrib.ML;

diff -r 03c4a5c08a79 -r 4200394242c5 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Wed Oct 03 20:58:27 2001 +0200
+++ b/src/Pure/IsaMakefile	Wed Oct 03 21:01:53 2001 +0200
@@ -30,7 +30,7 @@
   General/symbol.ML General/table.ML General/url.ML Interface/ROOT.ML	\
   Interface/isamode.ML Interface/proof_general.ML Isar/ROOT.ML Isar/antiquote.ML \
   Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML	\
-  Isar/comment.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_output.ML     \
+  Isar/comment.ML Isar/induct_attrib.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_output.ML     \
   Isar/isar_syn.ML Isar/isar_thy.ML Isar/local_defs.ML Isar/method.ML   \
   Isar/net_rules.ML Isar/obtain.ML Isar/outer_lex.ML Isar/outer_parse.ML \
   Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML		\
diff -r 03c4a5c08a79 -r 4200394242c5 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Wed Oct 03 20:58:27 2001 +0200
+++ b/src/Pure/Isar/ROOT.ML	Wed Oct 03 21:01:53 2001 +0200
@@ -16,6 +16,7 @@
 use "args.ML";
 use "attrib.ML";
 use "net_rules.ML";
+use "induct_attrib.ML";
 use "method.ML";
 
 (*derived proof elements*)
diff -r 03c4a5c08a79 -r 4200394242c5 src/Pure/Isar/induct_attrib.ML
--- a/src/Pure/Isar/induct_attrib.ML	Wed Oct 03 20:58:27 2001 +0200
+++ b/src/Pure/Isar/induct_attrib.ML	Wed Oct 03 21:01:53 2001 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/induct_attrib.ML
+(*  Title:      Pure/Isar/induct_attrib.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
@@ -59,11 +59,11 @@
   in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end;
 
 
-(* theory data kind 'HOL/induction' *)
+(* theory data kind 'Isar/induction' *)
 
 structure GlobalInductArgs =
 struct
-  val name = "HOL/induction";
+  val name = "Isar/induction";
   type T = (rules * rules) * (rules * rules);
 
   val empty = ((type_rules, set_rules), (type_rules, set_rules));
@@ -92,11 +92,11 @@
 val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
 
 
-(* proof data kind 'HOL/induction' *)
+(* proof data kind 'Isar/induction' *)
 
 structure LocalInductArgs =
 struct
-  val name = "HOL/induction";
+  val name = "Isar/induction";
   type T = GlobalInductArgs.T;
 
   fun init thy = GlobalInduct.get thy;
diff -r 03c4a5c08a79 -r 4200394242c5 src/Pure/pure.ML
--- a/src/Pure/pure.ML	Wed Oct 03 20:58:27 2001 +0200
+++ b/src/Pure/pure.ML	Wed Oct 03 21:01:53 2001 +0200
@@ -12,6 +12,7 @@
     ProofContext.setup @
     Attrib.setup @
     Method.setup @
+    InductAttrib.setup @
     Calculation.setup @
     SkipProof.setup @
     AxClass.setup @