# HG changeset patch
# User berghofe
# Date 1184147244 -7200
# Node ID 7bc32680a4952ad76d999feb9ff55249ee0adeb7
# Parent  d639647a1ffddae31bb49f696f8b31d2b5b6c6c6
Renamed inductive2 to inductive.

diff -r d639647a1ffd -r 7bc32680a495 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Wed Jul 11 11:47:13 2007 +0200
+++ b/src/HOL/Unix/Unix.thy	Wed Jul 11 11:47:24 2007 +0200
@@ -350,7 +350,7 @@
   involved here).
 *}
 
-inductive2
+inductive
   transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
     ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
 where
@@ -501,7 +501,7 @@
   amount of time.
 *}
 
-inductive2
+inductive
   transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
     ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
 where