# HG changeset patch
# User wenzelm
# Date 981401645 -3600
# Node ID 8f47967ecc80d0e8ec6109a2a4d00927238d6a26
# Parent  4e542a09b5825e9120d962cf8182068fb1160b33
tuned

diff -r 4e542a09b582 -r 8f47967ecc80 src/HOL/AxClasses/Group.thy
--- a/src/HOL/AxClasses/Group.thy	Mon Feb 05 20:33:50 2001 +0100
+++ b/src/HOL/AxClasses/Group.thy	Mon Feb 05 20:34:05 2001 +0100
@@ -10,7 +10,7 @@
 
 consts
   times :: "'a => 'a => 'a"    (infixl "[*]" 70)
-  inverse :: "'a => 'a"
+  invers :: "'a => 'a"
   one :: 'a
 
 
@@ -24,7 +24,7 @@
 
 axclass group < semigroup
   left_unit:    "one [*] x = x"
-  left_inverse: "inverse x [*] x = one"
+  left_inverse: "invers x [*] x = one"
 
 axclass agroup < group
   commute: "x [*] y = y [*] x"
@@ -32,21 +32,21 @@
 
 subsection {* Abstract reasoning *}
 
-theorem group_right_inverse: "x [*] inverse x = (one::'a::group)"
+theorem group_right_inverse: "x [*] invers x = (one::'a::group)"
 proof -
-  have "x [*] inverse x = one [*] (x [*] inverse x)"
+  have "x [*] invers x = one [*] (x [*] invers x)"
     by (simp only: group.left_unit)
-  also have "... = one [*] x [*] inverse x"
+  also have "... = one [*] x [*] invers x"
     by (simp only: semigroup.assoc)
-  also have "... = inverse (inverse x) [*] inverse x [*] x [*] inverse x"
+  also have "... = invers (invers x) [*] invers x [*] x [*] invers x"
     by (simp only: group.left_inverse)
-  also have "... = inverse (inverse x) [*] (inverse x [*] x) [*] inverse x"
+  also have "... = invers (invers x) [*] (invers x [*] x) [*] invers x"
     by (simp only: semigroup.assoc)
-  also have "... = inverse (inverse x) [*] one [*] inverse x"
+  also have "... = invers (invers x) [*] one [*] invers x"
     by (simp only: group.left_inverse)
-  also have "... = inverse (inverse x) [*] (one [*] inverse x)"
+  also have "... = invers (invers x) [*] (one [*] invers x)"
     by (simp only: semigroup.assoc)
-  also have "... = inverse (inverse x) [*] inverse x"
+  also have "... = invers (invers x) [*] invers x"
     by (simp only: group.left_unit)
   also have "... = one"
     by (simp only: group.left_inverse)
@@ -55,9 +55,9 @@
 
 theorem group_right_unit: "x [*] one = (x::'a::group)"
 proof -
-  have "x [*] one = x [*] (inverse x [*] x)"
+  have "x [*] one = x [*] (invers x [*] x)"
     by (simp only: group.left_inverse)
-  also have "... = x [*] inverse x [*] x"
+  also have "... = x [*] invers x [*] x"
     by (simp only: semigroup.assoc)
   also have "... = one [*] x"
     by (simp only: group_right_inverse)
@@ -92,7 +92,7 @@
 
 defs (overloaded)
   times_bool_def:   "x [*] y == x ~= (y::bool)"
-  inverse_bool_def: "inverse x == x::bool"
+  inverse_bool_def: "invers x == x::bool"
   unit_bool_def:    "one == False"
 
 instance bool :: agroup
diff -r 4e542a09b582 -r 8f47967ecc80 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Mon Feb 05 20:33:50 2001 +0100
+++ b/src/HOL/Unix/Unix.thy	Mon Feb 05 20:34:05 2001 +0100
@@ -259,7 +259,7 @@
 proof -
   assume "path' \<parallel> path"
   then obtain y z xs ys zs where
-    "y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs"
+      "y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs"
     by (blast dest: parallel_decomp)
   hence "lookup (update path' opt root) path = lookup root path"
     by (blast intro: lookup_update_other)
diff -r 4e542a09b582 -r 8f47967ecc80 src/HOL/Unix/document/root.bib
--- a/src/HOL/Unix/document/root.bib	Mon Feb 05 20:33:50 2001 +0100
+++ b/src/HOL/Unix/document/root.bib	Mon Feb 05 20:34:05 2001 +0100
@@ -1,6 +1,7 @@
 
 @Unpublished{Bauer-et-al:2001:HOL-Library,
-  author = 	 {Gertrud Bauer and Tobias Nipkow and Lawrence C Paulson and Markus Wenzel},
+  author = 	 {Gertrud Bauer and Tobias Nipkow and Lawrence C Paulson and
+                  Thomas M Rasmussen and Markus Wenzel},
   title = 	 {The Supplemental {Isabelle/HOL} Library},
   note = 	 {\url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
   year =	 2001