# HG changeset patch
# User wenzelm
# Date 1408191159 -7200
# Node ID 59c17b0b870d3b45cb4d85a02f17e552f9ebb479
# Parent  b203a7644bf1e82582c3c8bb40c46907e6e2c104
updated to named_theorems;

diff -r b203a7644bf1 -r 59c17b0b870d src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sat Aug 16 13:54:19 2014 +0200
+++ b/src/HOL/Fields.thy	Sat Aug 16 14:12:39 2014 +0200
@@ -25,15 +25,7 @@
 
 text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
 
-ML {*
-structure Divide_Simps = Named_Thms
-(
-  val name = @{binding divide_simps}
-  val description = "rewrite rules to eliminate divisions"
-)
-*}
-
-setup Divide_Simps.setup
+named_theorems divide_simps "rewrite rules to eliminate divisions"
 
 
 class division_ring = ring_1 + inverse +
diff -r b203a7644bf1 -r 59c17b0b870d src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sat Aug 16 13:54:19 2014 +0200
+++ b/src/HOL/Groups.thy	Sat Aug 16 14:12:39 2014 +0200
@@ -8,17 +8,10 @@
 imports Orderings
 begin
 
-subsection {* Fact collections *}
+subsection {* Dynamic facts *}
 
-ML {*
-structure Ac_Simps = Named_Thms
-(
-  val name = @{binding ac_simps}
-  val description = "associativity and commutativity simplification rules"
-)
-*}
+named_theorems ac_simps "associativity and commutativity simplification rules"
 
-setup Ac_Simps.setup
 
 text{* The rewrites accumulated in @{text algebra_simps} deal with the
 classical algebraic structures of groups, rings and family. They simplify
@@ -29,30 +22,15 @@
 Of course it also works for fields, but it knows nothing about multiplicative
 inverses or division. This is catered for by @{text field_simps}. *}
 
-ML {*
-structure Algebra_Simps = Named_Thms
-(
-  val name = @{binding algebra_simps}
-  val description = "algebra simplification rules"
-)
-*}
+named_theorems algebra_simps "algebra simplification rules"
 
-setup Algebra_Simps.setup
 
 text{* Lemmas @{text field_simps} multiply with denominators in (in)equations
 if they can be proved to be non-zero (for equations) or positive/negative
 (for inequations). Can be too aggressive and is therefore separate from the
 more benign @{text algebra_simps}. *}
 
-ML {*
-structure Field_Simps = Named_Thms
-(
-  val name = @{binding field_simps}
-  val description = "algebra simplification rules for fields"
-)
-*}
-
-setup Field_Simps.setup
+named_theorems field_simps "algebra simplification rules for fields"
 
 
 subsection {* Abstract structures *}