src/HOL/Groebner_Basis.thy
changeset 60758 d8d85a8172b5
parent 58925 1b655309617c
child 61476 1884c40f1539
     1.1 --- a/src/HOL/Groebner_Basis.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -2,17 +2,17 @@
     1.4      Author:     Amine Chaieb, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Groebner bases *}
     1.8 +section \<open>Groebner bases\<close>
     1.9  
    1.10  theory Groebner_Basis
    1.11  imports Semiring_Normalization Parity
    1.12  begin
    1.13  
    1.14 -subsection {* Groebner Bases *}
    1.15 +subsection \<open>Groebner Bases\<close>
    1.16  
    1.17 -lemmas bool_simps = simp_thms(1-34) -- {* FIXME move to @{theory HOL} *}
    1.18 +lemmas bool_simps = simp_thms(1-34) -- \<open>FIXME move to @{theory HOL}\<close>
    1.19  
    1.20 -lemma nnf_simps: -- {* FIXME shadows fact binding in @{theory HOL} *}
    1.21 +lemma nnf_simps: -- \<open>FIXME shadows fact binding in @{theory HOL}\<close>
    1.22    "(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)"
    1.23    "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
    1.24    "(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
    1.25 @@ -35,7 +35,7 @@
    1.26  named_theorems algebra "pre-simplification rules for algebraic methods"
    1.27  ML_file "Tools/groebner.ML"
    1.28  
    1.29 -method_setup algebra = {*
    1.30 +method_setup algebra = \<open>
    1.31    let
    1.32      fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
    1.33      val addN = "add"
    1.34 @@ -48,7 +48,7 @@
    1.35      (fn (add_ths, del_ths) => fn ctxt =>
    1.36        SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
    1.37    end
    1.38 -*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
    1.39 +\<close> "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
    1.40  
    1.41  declare dvd_def[algebra]
    1.42  declare dvd_eq_mod_eq_0[symmetric, algebra]