1.1 --- a/etc/isar-keywords.el	Fri Feb 19 09:35:18 2010 +0100
     1.2 +++ b/etc/isar-keywords.el	Fri Feb 19 11:06:20 2010 +0100
     1.3 @@ -55,6 +55,7 @@
     1.4      "classes"
     1.5      "classrel"
     1.6      "code_abort"
     1.7 +    "code_abstype"
     1.8      "code_class"
     1.9      "code_const"
    1.10      "code_datatype"
    1.11 @@ -537,6 +538,7 @@
    1.12  (defconst isar-keywords-theory-goal
    1.13    '("ax_specification"
    1.14      "boogie_vc"
    1.15 +    "code_abstype"
    1.16      "code_pred"
    1.17      "corollary"
    1.18      "cpodef"

     2.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Feb 19 09:35:18 2010 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Feb 19 11:06:20 2010 +0100
     2.3 @@ -479,6 +479,11 @@
     2.4    OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
     2.5      (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
     2.6  
     2.7 +val _ =
     2.8 +  OuterSyntax.command "code_abstype" "define abstract code type" K.thy_goal
     2.9 +    (P.term -- P.term >> (fn (abs, rep) => Toplevel.print
    2.10 +      o Toplevel.theory_to_proof (Code.add_abstype_cmd abs rep)));
    2.11 +
    2.12  
    2.13  
    2.14  (** proof commands **)