# HG changeset patch
# User wenzelm
# Date 1140110760 -3600
# Node ID e1948ebe9c7d24b0baff76672921a1a8d41f1a43
# Parent  12833c7e0fa63b6cdedcc593e325945e373d1830
added 'abbreviation';
tuned;

diff -r 12833c7e0fa6 -r e1948ebe9c7d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Feb 16 18:25:58 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Feb 16 18:26:00 2006 +0100
@@ -175,26 +175,35 @@
     (opt_overloaded -- Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_defs));
 
 
-(* constant definitions *)
-
-val structs =
-  Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
+(* constant definitions and abbreviations *)
 
 val constdecl =
   (P.name --| P.$$$ "where") >> (fn x => (x, NONE, 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 structs =
+  Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
+
 val constdefsP =
-  OuterSyntax.command "constdefs" "old-style constant definitions" K.thy_decl
+  OuterSyntax.command "constdefs" "old-style constant definition" K.thy_decl
     (structs -- Scan.repeat1 constdef >> (Toplevel.theory o Constdefs.add_constdefs));
 
 val definitionP =
-  OuterSyntax.command "definition" "standard constant definition" K.thy_decl
+  OuterSyntax.command "definition" "constant definition" K.thy_decl
     (P.opt_locale_target -- Scan.repeat1 constdef
     >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args)));
 
+val abbreviationP =
+  OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
+    (P.opt_locale_target --
+      Scan.optional (P.$$$ "(" -- P.$$$ "output" -- P.$$$ ")" >> K true) false --
+      Scan.repeat1 (Scan.option constdecl -- P.prop)
+    >> (fn ((loc, revert), args) =>
+         Toplevel.local_theory loc (Specification.abbreviation revert args)));
+
 
 (* constant specifications *)
 
@@ -860,11 +869,11 @@
   classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
   aritiesP, judgmentP, constsP, finalconstsP, syntaxP, no_syntaxP,
   translationsP, axiomsP, defsP, constdefsP, definitionP,
-  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,
+  abbreviationP, 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,