hide the rather generic names used in theory Commutative_Ring;
authorwenzelm
Wed Sep 14 23:14:58 2005 +0200 (2005-09-14)
changeset 17395a05e20f6a31a
parent 17394 a8c9ed3f9818
child 17396 1ca607b28670
hide the rather generic names used in theory Commutative_Ring;
src/HOL/Main.thy
     1.1 --- a/src/HOL/Main.thy	Wed Sep 14 23:14:57 2005 +0200
     1.2 +++ b/src/HOL/Main.thy	Wed Sep 14 23:14:58 2005 +0200
     1.3 @@ -15,6 +15,18 @@
     1.4    PreList} already includes most HOL theories.
     1.5  *}
     1.6  
     1.7 +
     1.8 +subsection {* Misc *}
     1.9 +
    1.10 +text {* Hide the rather generic names used in theory @{text Commutative_Ring}. *}
    1.11 +
    1.12 +hide (open) const
    1.13 +  Pc Pinj PX
    1.14 +  Pol Add Sub Mul Pow Neg
    1.15 +  add mul neg sqr pow sub
    1.16 +  norm
    1.17 +
    1.18 +
    1.19  subsection {* Configuration of the code generator *}
    1.20  
    1.21  types_code
    1.22 @@ -70,6 +82,7 @@
    1.23  
    1.24  lemmas [code] = imp_conv_disj
    1.25  
    1.26 +
    1.27  subsection {* Configuration of the 'refute' command *}
    1.28  
    1.29  text {*