src/HOL/Semiring_Normalization.thy
changeset 52435 6646bb548c6b
parent 48891 c0eafbd55de3
child 53076 47c9aff07725
equal deleted inserted replaced
52434:cbb94074682b 52435:6646bb548c6b
   217 hide_fact (open) normalizing_comm_ring_1_axioms
   217 hide_fact (open) normalizing_comm_ring_1_axioms
   218   normalizing_idom_axioms normalizing_ring_ops normalizing_ring_rules
   218   normalizing_idom_axioms normalizing_ring_ops normalizing_ring_rules
   219 
   219 
   220 hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules
   220 hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules
   221 
   221 
   222 code_modulename SML
   222 code_identifier
   223   Semiring_Normalization Arith
   223   code_module Semiring_Normalization \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   224 
   224 
   225 code_modulename OCaml
   225 end
   226   Semiring_Normalization Arith
       
   227 
       
   228 code_modulename Haskell
       
   229   Semiring_Normalization Arith
       
   230 
       
   231 end