updated to named_theorems;
authorwenzelm
Sat Aug 16 14:12:39 2014 +0200 (2014-08-16)
changeset 5795059c17b0b870d
parent 57949 b203a7644bf1
child 57951 7896762b638b
updated to named_theorems;
src/HOL/Fields.thy
src/HOL/Groups.thy
     1.1 --- a/src/HOL/Fields.thy	Sat Aug 16 13:54:19 2014 +0200
     1.2 +++ b/src/HOL/Fields.thy	Sat Aug 16 14:12:39 2014 +0200
     1.3 @@ -25,15 +25,7 @@
     1.4  
     1.5  text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
     1.6  
     1.7 -ML {*
     1.8 -structure Divide_Simps = Named_Thms
     1.9 -(
    1.10 -  val name = @{binding divide_simps}
    1.11 -  val description = "rewrite rules to eliminate divisions"
    1.12 -)
    1.13 -*}
    1.14 -
    1.15 -setup Divide_Simps.setup
    1.16 +named_theorems divide_simps "rewrite rules to eliminate divisions"
    1.17  
    1.18  
    1.19  class division_ring = ring_1 + inverse +
     2.1 --- a/src/HOL/Groups.thy	Sat Aug 16 13:54:19 2014 +0200
     2.2 +++ b/src/HOL/Groups.thy	Sat Aug 16 14:12:39 2014 +0200
     2.3 @@ -8,17 +8,10 @@
     2.4  imports Orderings
     2.5  begin
     2.6  
     2.7 -subsection {* Fact collections *}
     2.8 +subsection {* Dynamic facts *}
     2.9  
    2.10 -ML {*
    2.11 -structure Ac_Simps = Named_Thms
    2.12 -(
    2.13 -  val name = @{binding ac_simps}
    2.14 -  val description = "associativity and commutativity simplification rules"
    2.15 -)
    2.16 -*}
    2.17 +named_theorems ac_simps "associativity and commutativity simplification rules"
    2.18  
    2.19 -setup Ac_Simps.setup
    2.20  
    2.21  text{* The rewrites accumulated in @{text algebra_simps} deal with the
    2.22  classical algebraic structures of groups, rings and family. They simplify
    2.23 @@ -29,30 +22,15 @@
    2.24  Of course it also works for fields, but it knows nothing about multiplicative
    2.25  inverses or division. This is catered for by @{text field_simps}. *}
    2.26  
    2.27 -ML {*
    2.28 -structure Algebra_Simps = Named_Thms
    2.29 -(
    2.30 -  val name = @{binding algebra_simps}
    2.31 -  val description = "algebra simplification rules"
    2.32 -)
    2.33 -*}
    2.34 +named_theorems algebra_simps "algebra simplification rules"
    2.35  
    2.36 -setup Algebra_Simps.setup
    2.37  
    2.38  text{* Lemmas @{text field_simps} multiply with denominators in (in)equations
    2.39  if they can be proved to be non-zero (for equations) or positive/negative
    2.40  (for inequations). Can be too aggressive and is therefore separate from the
    2.41  more benign @{text algebra_simps}. *}
    2.42  
    2.43 -ML {*
    2.44 -structure Field_Simps = Named_Thms
    2.45 -(
    2.46 -  val name = @{binding field_simps}
    2.47 -  val description = "algebra simplification rules for fields"
    2.48 -)
    2.49 -*}
    2.50 -
    2.51 -setup Field_Simps.setup
    2.52 +named_theorems field_simps "algebra simplification rules for fields"
    2.53  
    2.54  
    2.55  subsection {* Abstract structures *}