fold / unfold methods;

--- a/src/Pure/Isar/method.ML	Tue Apr 27 15:14:22 1999 +0200
+++ b/src/Pure/Isar/method.ML	Tue Apr 27 15:14:44 1999 +0200
@@ -60,10 +60,10 @@
   val local_immediate_proof: Proof.state -> Proof.state Seq.seq
   val local_default_proof: Proof.state -> Proof.state Seq.seq
   val global_qed: bstring option -> theory attribute list option -> text option
-    -> Proof.state -> theory * (string * string * thm)
-  val global_terminal_proof: text -> Proof.state -> theory * (string * string * thm)
-  val global_immediate_proof: Proof.state -> theory * (string * string * thm)
-  val global_default_proof: Proof.state -> theory * (string * string * thm)
+    -> Proof.state -> theory * {kind: string, name: string, thm: thm}
+  val global_terminal_proof: text -> Proof.state -> theory * {kind: string, name: string, thm: thm}
+  val global_immediate_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
+  val global_default_proof: Proof.state -> theory * {kind: string, name: string, thm: thm}
   val setup: (theory -> theory) list
 end;
 
@@ -105,6 +105,12 @@
 val asm_finish = METHOD (K (FINISHED (ALLGOALS assume_tac)));
 
 
+(* fold / unfold definitions *)
+
+val fold = METHOD0 o fold_goals_tac;
+val unfold = METHOD0 o rewrite_goals_tac;
+
+
 (* rule *)
 
 fun res th i rule = Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty;
@@ -317,6 +323,8 @@
   ("same", no_args same, "insert facts, nothing else"),
   ("assumption", no_args assumption, "proof by assumption"),
   ("finish", no_args asm_finish, "finish proof by assumption"),
+  ("fold", thms_args fold, "fold definitions"),
+  ("unfold", thms_args unfold, "unfold definitions"),
   ("rule", thms_args rule, "apply primitive rule")];