unfold / fold defs;
authorwenzelm
Sat Sep 25 13:06:59 1999 +0200 (1999-09-25 ago)
changeset 7598af320257c902
parent 7597 4fbdb8a0c378
child 7599 40b7f7f51208
unfold / fold defs;
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat Sep 25 13:06:06 1999 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Sep 25 13:06:59 1999 +0200
     1.3 @@ -251,6 +251,16 @@
     1.4  val local_with = gen_with I;
     1.5  
     1.6  
     1.7 +(* unfold / fold definitions *)
     1.8 +
     1.9 +fun gen_rewrite rew defs (x, thm) = (x, rew defs thm);
    1.10 +
    1.11 +val global_unfold = syntax (global_thmss >> gen_rewrite Tactic.rewrite_rule);
    1.12 +val local_unfold = syntax (local_thmss >> gen_rewrite Tactic.rewrite_rule);
    1.13 +val global_fold = syntax (global_thmss >> gen_rewrite Tactic.fold_rule);
    1.14 +val local_fold = syntax (local_thmss >> gen_rewrite Tactic.fold_rule);
    1.15 +
    1.16 +
    1.17  (* misc rules *)
    1.18  
    1.19  fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
    1.20 @@ -273,6 +283,8 @@
    1.21    ("OF", (global_APP, local_APP), "resolve with rule -- apply rule to rules"),
    1.22    ("where", (global_where, local_where), "named instantiation of theorem"),
    1.23    ("of", (global_with, local_with), "positional instantiation of theorem -- apply rule to terms"),
    1.24 +  ("unfold", (global_unfold, local_unfold), "unfold definitions"),
    1.25 +  ("fold", (global_fold, local_fold), "fold definitions"),
    1.26    ("standard", (standard, standard), "put theorem into standard form"),
    1.27    ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"),
    1.28    ("transfer", (global_transfer, local_transfer), "transfer theorem to this theory"),