# HG changeset patch
# User wenzelm
# Date 894989223 -7200
# Node ID 119d5f5767a4877d16bafcc6b242d66ac08396e6
# Parent  44c6f462c8fac64c62c2b2c1b79de70f63247d7a
added Goal, Goalw;

diff -r 44c6f462c8fa -r 119d5f5767a4 src/Pure/Thy/context.ML
--- a/src/Pure/Thy/context.ML	Tue May 12 18:06:27 1998 +0200
+++ b/src/Pure/Thy/context.ML	Tue May 12 18:07:03 1998 +0200
@@ -15,6 +15,8 @@
   val reset_context: unit -> unit
   val thm: xstring -> thm
   val thms: xstring -> thm list
+  val Goal: string -> thm list
+  val Goalw: thm list -> string -> thm list
 end;
 
 signature CONTEXT =
@@ -62,6 +64,12 @@
 fun thms name = PureThy.get_thms (get_context ()) name;
 
 
+(* shortcut goal commands *)
+
+fun Goal s = Goals.goal (get_context ()) s;
+fun Goalw thms s = Goals.goalw (get_context ()) thms s;
+
+
 end;