src/Pure/Isar/isar_syn.ML
changeset 24589 d3fca349736c
parent 24451 7c205d006719
child 24624 b8383b1bbae3
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Sep 15 19:27:43 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Sep 15 19:27:44 2007 +0200
     1.3 @@ -427,13 +427,24 @@
     1.4  val instanceP =
     1.5    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
     1.6        P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
     1.7 -           >> Class.instance_class_cmd
     1.8 +           >> Class.classrel_cmd
     1.9        || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    1.10 -           >> Class.instance_sort_cmd
    1.11 +           >> Class.interpretation_in_class_cmd
    1.12        || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    1.13 -           >> (fn (arities, defs) => Class.instance_arity_cmd arities defs (fold (Code.add_func false)))
    1.14 +           >> (fn (arities, defs) => Class.instance_cmd arities defs (fold (Code.add_func false)))
    1.15      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.16  
    1.17 +val instantiationP =
    1.18 +  OuterSyntax.command "instantiation" "prove type arity" K.thy_decl (
    1.19 +      P.and_list1 P.arity -- P.opt_begin
    1.20 +           >> (fn (arities, begin) => (begin ? Toplevel.print)
    1.21 +            o Toplevel.begin_local_theory begin
    1.22 +                (Instance.begin_instantiation_cmd arities)));
    1.23 +
    1.24 +val instance_proofP =
    1.25 +  OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal
    1.26 +      (Scan.succeed ((Toplevel.print oo Toplevel.local_theory_to_proof NONE) Instance.proof_instantiation));
    1.27 +
    1.28  end;
    1.29  
    1.30  
    1.31 @@ -993,7 +1004,7 @@
    1.32    simproc_setupP, parse_ast_translationP, parse_translationP,
    1.33    print_translationP, typed_print_translationP,
    1.34    print_ast_translationP, token_translationP, oracleP, contextP,
    1.35 -  localeP, classP, instanceP, code_datatypeP,
    1.36 +  localeP, classP, instanceP, instantiationP, instance_proofP, code_datatypeP,
    1.37    (*proof commands*)
    1.38    theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
    1.39    assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,