# HG changeset patch
# User wenzelm
# Date 931451711 -7200
# Node ID 0890fde415227753858c963fbe3dfe1a3c73bb32
# Parent  77c14313af5195e080d044d7df950fa6942b56d8
'export';

diff -r 77c14313af51 -r 0890fde41522 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Jul 08 18:34:59 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Jul 08 18:35:11 1999 +0200
@@ -251,6 +251,9 @@
 fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
 fun elimify x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
 
+fun global_export x = no_args (Drule.rule_attribute (Proof.export_thm o ProofContext.init)) x;
+fun local_export x = no_args (Drule.rule_attribute Proof.export_thm) x;
+
 
 
 (** theory setup **)
@@ -267,7 +270,8 @@
   ("of", (global_with, local_with), "positional instantiation of theorem -- apply rule to terms"),
   ("standard", (standard, standard), "put theorem into standard form"),
   ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"),
-  ("transfer", (global_transfer, local_transfer), "transfer theorem to this theory")];
+  ("transfer", (global_transfer, local_transfer), "transfer theorem to this theory"),
+  ("export", (global_export, local_export), "export theorem from context")];
 
 
 (* setup *)