# HG changeset patch
# User wenzelm
# Date 1136672876 -3600
# Node ID cf5d07758d3f54913b1cf77f2c2c8f7776b764b2
# Parent  2f3c24533aea59bb344f8ecffde560c85089c7f9
added 'axiomatization';

diff -r 2f3c24533aea -r cf5d07758d3f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Jan 07 23:27:55 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Jan 07 23:27:56 2006 +0100
@@ -186,7 +186,6 @@
   (P.name --| P.$$$ "where") >> (fn x => (x, NONE, Syntax.NoSyn)) ||
     P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix' >> P.triple1 ||
     P.name -- (P.mixfix' >> pair NONE) >> P.triple2;
-
 val constdef = Scan.option constdecl -- (P.opt_thm_name ":" -- P.prop);
 
 val constdefsP =
@@ -194,6 +193,14 @@
     (structs -- Scan.repeat1 constdef >> (Toplevel.theory o Constdefs.add_constdefs));
 
 
+(* constant specifications *)
+
+val axiomatizationP =
+  OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
+    (P.and_list1 P.param -- Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.named_spec)) []
+    >> (Toplevel.theory o (#2 oo Specification.axiomatize)));
+
+
 (* theorems *)
 
 fun theorems kind = P.opt_locale_target -- P.name_facts
@@ -851,11 +858,12 @@
   (*theory sections*)
   classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
   aritiesP, judgmentP, constsP, finalconstsP, syntaxP, no_syntaxP,
-  translationsP, axiomsP, defsP, constdefsP, theoremsP, lemmasP,
-  declareP, globalP, localP, hideP, useP, mlP, ml_commandP, ml_setupP,
-  setupP, method_setupP, parse_ast_translationP, parse_translationP,
-  print_translationP, typed_print_translationP,
-  print_ast_translationP, token_translationP, oracleP, localeP,
+  translationsP, axiomsP, defsP, constdefsP, axiomatizationP,
+  theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP,
+  ml_commandP, ml_setupP, setupP, method_setupP,
+  parse_ast_translationP, parse_translationP, print_translationP,
+  typed_print_translationP, print_ast_translationP,
+  token_translationP, oracleP, localeP,
   (*proof commands*)
   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
   assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,