src/Pure/Isar/proof.ML
changeset 14508 859b11514537
parent 14404 4952c5a92e04
child 14528 1457584110ac
     1.1 --- a/src/Pure/Isar/proof.ML	Fri Apr 02 12:25:48 2004 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Apr 02 14:08:30 2004 +0200
     1.3 @@ -65,6 +65,7 @@
     1.4      (thm list * context attribute list) list) list -> state -> state
     1.5    val using_thmss: ((xstring * context attribute list) list) list -> state -> state
     1.6    val using_thmss_i: ((thm list * context attribute list) list) list -> state -> state
     1.7 +  val instantiate_locale: string * string -> state -> state
     1.8    val fix: (string list * string option) list -> state -> state
     1.9    val fix_i: (string list * typ option) list -> state -> state
    1.10    val assm: ProofContext.exporter
    1.11 @@ -510,6 +511,7 @@
    1.12  
    1.13  
    1.14  (* have_thmss *)
    1.15 +(* CB: this implements "note" of the Isar/VM *)
    1.16  
    1.17  local
    1.18  
    1.19 @@ -565,6 +567,19 @@
    1.20  end;
    1.21  
    1.22  
    1.23 +(* locale instantiation *)
    1.24 +
    1.25 +fun instantiate_locale (loc_name, prfx) state = let
    1.26 +    val ctxt = context_of state;
    1.27 +    val facts = if is_chain state then get_facts state else None;
    1.28 +  in
    1.29 +    state
    1.30 +    |> assert_forward_or_chain
    1.31 +    |> enter_forward
    1.32 +    |> reset_facts
    1.33 +    |> map_context (Locale.instantiate loc_name prfx facts)
    1.34 +  end;
    1.35 +
    1.36  (* fix *)
    1.37  
    1.38  fun gen_fix f xs state =