# HG changeset patch
# User berghofe
# Date 1184147548 -7200
# Node ID 8b37b6615c5257739ceff7728b126ee53b745b8c
# Parent  07968f8cc6622ddab3e3c7ed389ed92005a4fd5f
Renamed inductive2 to inductive.

diff -r 07968f8cc662 -r 8b37b6615c52 src/HOL/ex/Abstract_NAT.thy
--- a/src/HOL/ex/Abstract_NAT.thy	Wed Jul 11 11:52:00 2007 +0200
+++ b/src/HOL/ex/Abstract_NAT.thy	Wed Jul 11 11:52:28 2007 +0200
@@ -26,7 +26,7 @@
 
 text {* \medskip Primitive recursion as a (functional) relation -- polymorphic! *}
 
-inductive2
+inductive
   Rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a \<Rightarrow> bool"
   for e :: 'a and r :: "'n \<Rightarrow> 'a \<Rightarrow> 'a"
 where