src/Pure/Isar/isar_syn.ML
changeset 14508 859b11514537
parent 14223 0ee05eef881b
child 14528 1457584110ac
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Apr 02 12:25:48 2004 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 02 14:08:30 2004 +0200
     1.3 @@ -357,6 +357,12 @@
     1.4    OuterSyntax.command "using" "augment goal facts" K.prf_decl
     1.5      (facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.using_facts)));
     1.6  
     1.7 +val instantiateP =
     1.8 +  OuterSyntax.command "instantiate" "instantiate locale" K.prf_decl
     1.9 +    (P.name --| P.$$$ ":" -- P.xname
    1.10 +(*    (P.xname -- (P.$$$ "[" |-- P.name --| P.$$$ "]") *)
    1.11 +      >> (Toplevel.print oo (Toplevel.proof o IsarThy.instantiate_locale)));
    1.12 +
    1.13  
    1.14  (* proof context *)
    1.15  
    1.16 @@ -756,7 +762,7 @@
    1.17    default_proofP, immediate_proofP, done_proofP, skip_proofP,
    1.18    forget_proofP, deferP, preferP, applyP, apply_endP, proofP, alsoP,
    1.19    finallyP, moreoverP, ultimatelyP, backP, cannot_undoP, clear_undosP,
    1.20 -  redoP, undos_proofP, undoP, killP,
    1.21 +  redoP, undos_proofP, undoP, killP, instantiateP,
    1.22    (*diagnostic commands*)
    1.23    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    1.24    print_syntaxP, print_theoremsP, print_localesP, print_localeP,