# HG changeset patch
# User wenzelm
# Date 938257619 -7200
# Node ID af320257c9025a39bb05216ea7a40c95e1b6164e
# Parent  4fbdb8a0c3785ec358774fdadc38f6bdbc8f776b
unfold / fold defs;

diff -r 4fbdb8a0c378 -r af320257c902 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Sep 25 13:06:06 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Sep 25 13:06:59 1999 +0200
@@ -251,6 +251,16 @@
 val local_with = gen_with I;
 
 
+(* unfold / fold definitions *)
+
+fun gen_rewrite rew defs (x, thm) = (x, rew defs thm);
+
+val global_unfold = syntax (global_thmss >> gen_rewrite Tactic.rewrite_rule);
+val local_unfold = syntax (local_thmss >> gen_rewrite Tactic.rewrite_rule);
+val global_fold = syntax (global_thmss >> gen_rewrite Tactic.fold_rule);
+val local_fold = syntax (local_thmss >> gen_rewrite Tactic.fold_rule);
+
+
 (* misc rules *)
 
 fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
@@ -273,6 +283,8 @@
   ("OF", (global_APP, local_APP), "resolve with rule -- apply rule to rules"),
   ("where", (global_where, local_where), "named instantiation of theorem"),
   ("of", (global_with, local_with), "positional instantiation of theorem -- apply rule to terms"),
+  ("unfold", (global_unfold, local_unfold), "unfold definitions"),
+  ("fold", (global_fold, local_fold), "fold definitions"),
   ("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"),