--- 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"
--- 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
--- 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)"