src/HOL/Groups.thy
changeset 57950 59c17b0b870d
parent 57571 d38a98f496dd
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Groups.thy	Sat Aug 16 13:54:19 2014 +0200
     1.2 +++ b/src/HOL/Groups.thy	Sat Aug 16 14:12:39 2014 +0200
     1.3 @@ -8,17 +8,10 @@
     1.4  imports Orderings
     1.5  begin
     1.6  
     1.7 -subsection {* Fact collections *}
     1.8 +subsection {* Dynamic facts *}
     1.9  
    1.10 -ML {*
    1.11 -structure Ac_Simps = Named_Thms
    1.12 -(
    1.13 -  val name = @{binding ac_simps}
    1.14 -  val description = "associativity and commutativity simplification rules"
    1.15 -)
    1.16 -*}
    1.17 +named_theorems ac_simps "associativity and commutativity simplification rules"
    1.18  
    1.19 -setup Ac_Simps.setup
    1.20  
    1.21  text{* The rewrites accumulated in @{text algebra_simps} deal with the
    1.22  classical algebraic structures of groups, rings and family. They simplify
    1.23 @@ -29,30 +22,15 @@
    1.24  Of course it also works for fields, but it knows nothing about multiplicative
    1.25  inverses or division. This is catered for by @{text field_simps}. *}
    1.26  
    1.27 -ML {*
    1.28 -structure Algebra_Simps = Named_Thms
    1.29 -(
    1.30 -  val name = @{binding algebra_simps}
    1.31 -  val description = "algebra simplification rules"
    1.32 -)
    1.33 -*}
    1.34 +named_theorems algebra_simps "algebra simplification rules"
    1.35  
    1.36 -setup Algebra_Simps.setup
    1.37  
    1.38  text{* Lemmas @{text field_simps} multiply with denominators in (in)equations
    1.39  if they can be proved to be non-zero (for equations) or positive/negative
    1.40  (for inequations). Can be too aggressive and is therefore separate from the
    1.41  more benign @{text algebra_simps}. *}
    1.42  
    1.43 -ML {*
    1.44 -structure Field_Simps = Named_Thms
    1.45 -(
    1.46 -  val name = @{binding field_simps}
    1.47 -  val description = "algebra simplification rules for fields"
    1.48 -)
    1.49 -*}
    1.50 -
    1.51 -setup Field_Simps.setup
    1.52 +named_theorems field_simps "algebra simplification rules for fields"
    1.53  
    1.54  
    1.55  subsection {* Abstract structures *}