added triv_goal, rev_triv_goal (for Isar);

--- a/src/Pure/drule.ML	Sat Apr 04 11:42:26 1998 +0200
+++ b/src/Pure/drule.ML	Sat Apr 04 11:42:48 1998 +0200
@@ -70,6 +70,8 @@
   val triv_forall_equality: thm
   val swap_prems_rl     : thm
   val equal_intr_rule   : thm
+  val triv_goal: thm
+  val rev_triv_goal: thm
   val instantiate': ctyp option list -> cterm option list -> thm -> thm
 end;
 
@@ -571,6 +573,18 @@
   end;
 
 
+(* GOAL (PROP A) <==> PROP A *)
+
+local
+  val A = read_prop "PROP A";
+  val G = read_prop "GOAL (PROP A)";
+  val (G_def, _) = freeze_thaw ProtoPure.Goal_def;
+in
+  val triv_goal = store_thm "triv_goal" (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume A));
+  val rev_triv_goal = store_thm "rev_triv_goal" (Thm.equal_elim G_def (Thm.assume G));
+end;
+
+
 
 (** instantiate' rule **)