tuned document;
authorwenzelm
Tue Jun 05 22:46:53 2007 +0200 (2007-06-05)
changeset 2326650f0a4f12ed3
parent 23265 a6992b91fdde
child 23267 51c605f34c7f
tuned document;
src/HOL/Groebner_Basis.thy
src/HOL/ex/Codegenerator.thy
src/HOL/ex/Commutative_Ring_Complete.thy
     1.1 --- a/src/HOL/Groebner_Basis.thy	Tue Jun 05 20:46:25 2007 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Jun 05 22:46:53 2007 +0200
     1.3 @@ -259,7 +259,7 @@
     1.4  *} "Semiring_normalizer"
     1.5  
     1.6  
     1.7 -subsection {* Gröbner Bases *}
     1.8 +subsection {* Groebner Bases *}
     1.9  
    1.10  locale semiringb = gb_semiring +
    1.11    assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z"
     2.1 --- a/src/HOL/ex/Codegenerator.thy	Tue Jun 05 20:46:25 2007 +0200
     2.2 +++ b/src/HOL/ex/Codegenerator.thy	Tue Jun 05 22:46:53 2007 +0200
     2.3 @@ -11,4 +11,4 @@
     2.4  code_gen "*" in SML in OCaml file - in OCaml file -
     2.5  code_gen in SML in OCaml file - in OCaml file -
     2.6  
     2.7 -end
     2.8 \ No newline at end of file
     2.9 +end
     3.1 --- a/src/HOL/ex/Commutative_Ring_Complete.thy	Tue Jun 05 20:46:25 2007 +0200
     3.2 +++ b/src/HOL/ex/Commutative_Ring_Complete.thy	Tue Jun 05 22:46:53 2007 +0200
     3.3 @@ -70,7 +70,7 @@
     3.4    from prems show ?thesis by(cases x, auto)
     3.5  qed
     3.6  
     3.7 -text {* mkPX conserves normalizedness (_cn) *}
     3.8 +text {* mkPX conserves normalizedness (@{text "_cn"}) *}
     3.9  lemma mkPX_cn: 
    3.10    assumes "x \<noteq> 0" and "isnorm P" and "isnorm Q" 
    3.11    shows "isnorm (mkPX P x Q)"