# HG changeset patch
# User wenzelm
# Date 1164892642 -3600
# Node ID 6588b947d631b086f79cfed865ecd2f5766b29a7
# Parent  222810ce6b059dee7b3dbf2f2a66ce4b0d29256f
simplified syntax for 'definition', 'abbreviation';

diff -r 222810ce6b05 -r 6588b947d631 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Wed Nov 29 23:33:09 2006 +0100
+++ b/doc-src/IsarRef/generic.tex	Thu Nov 30 14:17:22 2006 +0100
@@ -23,19 +23,21 @@
 available, and result names need not be given.
 
 \begin{rail}
-  'axiomatization' target? consts? ('where' specs)?
+  'axiomatization' target? fixes? ('where' specs)?
   ;
-  'definition' target? (constdecl? constdef +)
+  'definition' target? (decl 'where')? thmdecl? prop
   ;
-  'abbreviation' target? mode? (constdecl? prop +)
+  'abbreviation' target? mode? (decl 'where')? prop
   ;
   'notation' target? mode? (nameref mixfix + 'and')
   ;
 
-  consts: ((name ('::' type)? structmixfix? | vars) + 'and')
+  fixes: ((name ('::' type)? mixfix? | vars) + 'and')
   ;
   specs: (thmdecl? props + 'and')
   ;
+  decl: name ('::' type)? mixfix?
+  ;
 \end{rail}
 
 \begin{descr}
diff -r 222810ce6b05 -r 6588b947d631 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Wed Nov 29 23:33:09 2006 +0100
+++ b/src/HOL/Library/State_Monad.thy	Thu Nov 30 14:17:22 2006 +0100
@@ -256,7 +256,7 @@
 subsection {* Combinators *}
 
 definition
-  lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c"
+  lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where
   "lift f x = return (f x)"
 
 fun
diff -r 222810ce6b05 -r 6588b947d631 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Nov 29 23:33:09 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 30 14:17:22 2006 +0100
@@ -188,32 +188,43 @@
       >> (Toplevel.theory o IsarCmd.add_defs));
 
 
-(* constant definitions and abbreviations *)
+(* old constdefs *)
 
-val constdecl =
-  (P.name --| P.$$$ "where") >> (fn x => (x, NONE, NoSyn)) ||
-    P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
-      --| Scan.option (P.$$$ "where") >> P.triple1 ||
-    P.name -- (P.mixfix >> pair NONE) --| Scan.option (P.$$$ "where") >> P.triple2;
+val old_constdecl =
+  P.name --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
+  P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
+    --| Scan.option P.where_ >> P.triple1 ||
+  P.name -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
 
-val constdef = Scan.option constdecl -- (P.opt_thm_name ":" -- P.prop);
+val old_constdef = Scan.option old_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 definition" K.thy_decl
-    (structs -- Scan.repeat1 constdef >> (Toplevel.theory o Constdefs.add_constdefs));
+    (structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
+
+
+(* constant definitions and abbreviations *)
+
+val constdecl =
+  P.name --
+    (P.where_ >> K (NONE, NoSyn) ||
+      P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
+      Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
+  >> P.triple2;
+
+val constdef = Scan.option constdecl -- (P.opt_thm_name ":" -- P.prop);
 
 val definitionP =
   OuterSyntax.command "definition" "constant definition" K.thy_decl
-    (P.opt_locale_target -- Scan.repeat1 constdef
+    (P.opt_locale_target -- (constdef >> single)
     >> (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 -- opt_mode --
-      Scan.repeat1 (Scan.option constdecl -- P.prop)
+    (P.opt_locale_target -- opt_mode -- (Scan.option constdecl -- P.prop >> single)
     >> (fn ((loc, mode), args) =>
         Toplevel.local_theory loc (Specification.abbreviation mode args)));
 
@@ -230,7 +241,7 @@
   OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
     (P.opt_locale_target --
      (Scan.optional P.fixes [] --
-      Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.spec)) [])
+      Scan.optional (P.where_ |-- P.!!! (P.and_list1 P.spec)) [])
     >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y)));
 
 
@@ -481,7 +492,7 @@
 val obtainP =
   OuterSyntax.command "obtain" "generalized existence"
     (K.tag_proof K.prf_asm_goal)
-    (P.parname -- Scan.optional (P.fixes --| P.$$$ "where") [] -- P.statement
+    (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- P.statement
       >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
 
 val guessP =