# HG changeset patch
# User wenzelm
# Date 1003082945 -7200
# Node ID 41ae2eb50bbfe09cdc6cec1b0e10ea1524a5611c
# Parent  7aa0702d33405d952e59094dfa88ec62860513ad
added 'atomize' attribute;

diff -r 7aa0702d3340 -r 41ae2eb50bbf src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Oct 14 20:08:42 2001 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Oct 14 20:09:05 2001 +0200
@@ -288,7 +288,6 @@
 fun exported_local x = no_args (Drule.rule_attribute Proof.export_thm) x;
 
 
-
 (** theory setup **)
 
 (* pure_attributes *)
@@ -309,7 +308,9 @@
   ("consumes", (consumes, consumes), "number of consumed facts"),
   ("case_names", (case_names, case_names), "named rule cases"),
   ("params", (params, params), "named rule parameters"),
-  ("exported", (exported_global, exported_local), "theorem exported from context")];
+  ("exported", (exported_global, exported_local), "theorem exported from context"),
+  ("atomize", (no_args ObjectLogic.atomize, no_args undef_local_attribute),
+    "declaration of atomize rule")];
 
 
 (* setup *)