# HG changeset patch
# User berghofe
# Date 1184144446 -7200
# Node ID bf8d4a46452d850a1865a434c18dd4869d7a2c8b
# Parent  afc12f93f64fe80d36b29e226a46dfa22f61a1bc
Renamed inductive2 to inductive.

diff -r afc12f93f64f -r bf8d4a46452d src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Jul 11 11:00:09 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Jul 11 11:00:46 2007 +0200
@@ -12,7 +12,7 @@
 
 subsection {* Definition and basic properties *}
 
-inductive2 finite :: "'a set => bool"
+inductive finite :: "'a set => bool"
   where
     emptyI [simp, intro!]: "finite {}"
   | insertI [simp, intro!]: "finite A ==> finite (insert a A)"
@@ -427,7 +427,7 @@
 se the definitions of sums and products over finite sets.
 *}
 
-inductive2
+inductive
   foldSet :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a => bool"
   for f ::  "'a => 'a => 'a"
   and g :: "'b => 'a"
@@ -438,7 +438,7 @@
      "\<lbrakk> x \<notin> A; foldSet f g z A y \<rbrakk>
       \<Longrightarrow> foldSet f g z (insert x A) (f (g x) y)"
 
-inductive_cases2 empty_foldSetE [elim!]: "foldSet f g z {} x"
+inductive_cases empty_foldSetE [elim!]: "foldSet f g z {} x"
 
 constdefs
   fold :: "('a => 'a => 'a) => ('b => 'a) => 'a => 'b set => 'a"
@@ -1794,7 +1794,7 @@
 
 text{* Does not require start value. *}
 
-inductive2
+inductive
   fold1Set :: "('a => 'a => 'a) => 'a set => 'a => bool"
   for f :: "'a => 'a => 'a"
 where
@@ -1809,9 +1809,9 @@
   "fold1Set f A x \<Longrightarrow> A \<noteq> {}"
   by(erule fold1Set.cases, simp_all) 
 
-inductive_cases2 empty_fold1SetE [elim!]: "fold1Set f {} x"
-
-inductive_cases2 insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"
+inductive_cases empty_fold1SetE [elim!]: "fold1Set f {} x"
+
+inductive_cases insert_fold1SetE [elim!]: "fold1Set f (insert a X) x"
 
 
 lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)"