# HG changeset patch
# User haftmann
# Date 1266573980 -3600
# Node ID 9f35be9c296016559b190f7c31bdf391196aa4f0
# Parent  5cb63cb4213f20c183e56ec701dcb6d64cdc11a7
added code_abstype keyword

diff -r 5cb63cb4213f -r 9f35be9c2960 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Feb 19 09:35:18 2010 +0100
+++ b/etc/isar-keywords.el	Fri Feb 19 11:06:20 2010 +0100
@@ -55,6 +55,7 @@
     "classes"
     "classrel"
     "code_abort"
+    "code_abstype"
     "code_class"
     "code_const"
     "code_datatype"
@@ -537,6 +538,7 @@
 (defconst isar-keywords-theory-goal
   '("ax_specification"
     "boogie_vc"
+    "code_abstype"
     "code_pred"
     "corollary"
     "cpodef"
diff -r 5cb63cb4213f -r 9f35be9c2960 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Feb 19 09:35:18 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Feb 19 11:06:20 2010 +0100
@@ -479,6 +479,11 @@
   OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
     (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
 
+val _ =
+  OuterSyntax.command "code_abstype" "define abstract code type" K.thy_goal
+    (P.term -- P.term >> (fn (abs, rep) => Toplevel.print
+      o Toplevel.theory_to_proof (Code.add_abstype_cmd abs rep)));
+
 
 
 (** proof commands **)