# HG changeset patch
# User wenzelm
# Date 1181076413 -7200
# Node ID 50f0a4f12ed3670d3e65aaa41da82a1487d7f329
# Parent  a6992b91fdde734b1e918cb668cb7f3237b9a6b8
tuned document;

diff -r a6992b91fdde -r 50f0a4f12ed3 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Tue Jun 05 20:46:25 2007 +0200
+++ b/src/HOL/Groebner_Basis.thy	Tue Jun 05 22:46:53 2007 +0200
@@ -259,7 +259,7 @@
 *} "Semiring_normalizer"
 
 
-subsection {* Gröbner Bases *}
+subsection {* Groebner Bases *}
 
 locale semiringb = gb_semiring +
   assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z"
diff -r a6992b91fdde -r 50f0a4f12ed3 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Tue Jun 05 20:46:25 2007 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Tue Jun 05 22:46:53 2007 +0200
@@ -11,4 +11,4 @@
 code_gen "*" in SML in OCaml file - in OCaml file -
 code_gen in SML in OCaml file - in OCaml file -
 
-end
\ No newline at end of file
+end
diff -r a6992b91fdde -r 50f0a4f12ed3 src/HOL/ex/Commutative_Ring_Complete.thy
--- a/src/HOL/ex/Commutative_Ring_Complete.thy	Tue Jun 05 20:46:25 2007 +0200
+++ b/src/HOL/ex/Commutative_Ring_Complete.thy	Tue Jun 05 22:46:53 2007 +0200
@@ -70,7 +70,7 @@
   from prems show ?thesis by(cases x, auto)
 qed
 
-text {* mkPX conserves normalizedness (_cn) *}
+text {* mkPX conserves normalizedness (@{text "_cn"}) *}
 lemma mkPX_cn: 
   assumes "x \<noteq> 0" and "isnorm P" and "isnorm Q" 
   shows "isnorm (mkPX P x Q)"