# HG changeset patch # User wenzelm # Date 902247874 -7200 # Node ID 9d7e6f7110ef80a7e651cac2c43f575a763ff69a # Parent 6b04b9a88c21927bb9530252289998fd92bd8de9 added Open_locale, Close_locale; thm(s): use Locale.get_thm(s); diff -r 6b04b9a88c21 -r 9d7e6f7110ef src/Pure/Thy/context.ML --- a/src/Pure/Thy/context.ML Tue Aug 04 18:23:57 1998 +0200 +++ b/src/Pure/Thy/context.ML Tue Aug 04 18:24:34 1998 +0200 @@ -13,6 +13,8 @@ val thms: xstring -> thm list val Goal: string -> thm list val Goalw: thm list -> string -> thm list + val Open_locale: xstring -> unit + val Close_locale: unit -> unit end; signature CONTEXT = @@ -73,8 +75,8 @@ (* retrieve thms *) -fun thm name = PureThy.get_thm (the_context ()) name; -fun thms name = PureThy.get_thms (the_context ()) name; +fun thm name = Locale.get_thm (the_context ()) name; +fun thms name = Locale.get_thms (the_context ()) name; (* shortcut goal commands *) @@ -83,6 +85,12 @@ fun Goalw thms s = Goals.atomic_goalw (the_context ()) thms s; +(* scope manipulation *) + +fun Open_locale xname = (Locale.open_locale xname (the_context ()); ()); +fun Close_locale () = (Locale.close_locale (the_context ()); ()); + + end;