--- a/src/Pure/goal.ML Thu Nov 30 14:17:27 2006 +0100
+++ b/src/Pure/goal.ML Thu Nov 30 14:17:29 2006 +0100
@@ -17,6 +17,8 @@
val protect: thm -> thm
val conclude: thm -> thm
val finish: thm -> thm
+ val norm_result: thm -> thm
+ val close_result: thm -> thm
val compose_hhf: thm -> int -> thm -> thm Seq.seq
val compose_hhf_tac: thm -> int -> tactic
val comp_hhf: thm -> thm -> thm
@@ -77,6 +79,19 @@
(** results **)
+(* normal form *)
+
+val norm_result =
+ Drule.flexflex_unique
+ #> MetaSimplifier.norm_hhf_protect
+ #> Thm.strip_shyps
+ #> Drule.zero_var_indexes;
+
+val close_result =
+ Thm.compress
+ #> Drule.close_derivation;
+
+
(* composition of normal results *)
fun compose_hhf tha i thb =