simplified syntax for 'definition', 'abbreviation';
authorwenzelm
Thu Nov 30 14:17:22 2006 +0100 (2006-11-30)
changeset 216016588b947d631
parent 21600 222810ce6b05
child 21602 cb13024d0e36
simplified syntax for 'definition', 'abbreviation';
doc-src/IsarRef/generic.tex
src/HOL/Library/State_Monad.thy
src/Pure/Isar/isar_syn.ML
     1.1 --- a/doc-src/IsarRef/generic.tex	Wed Nov 29 23:33:09 2006 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Thu Nov 30 14:17:22 2006 +0100
     1.3 @@ -23,19 +23,21 @@
     1.4  available, and result names need not be given.
     1.5  
     1.6  \begin{rail}
     1.7 -  'axiomatization' target? consts? ('where' specs)?
     1.8 +  'axiomatization' target? fixes? ('where' specs)?
     1.9    ;
    1.10 -  'definition' target? (constdecl? constdef +)
    1.11 +  'definition' target? (decl 'where')? thmdecl? prop
    1.12    ;
    1.13 -  'abbreviation' target? mode? (constdecl? prop +)
    1.14 +  'abbreviation' target? mode? (decl 'where')? prop
    1.15    ;
    1.16    'notation' target? mode? (nameref mixfix + 'and')
    1.17    ;
    1.18  
    1.19 -  consts: ((name ('::' type)? structmixfix? | vars) + 'and')
    1.20 +  fixes: ((name ('::' type)? mixfix? | vars) + 'and')
    1.21    ;
    1.22    specs: (thmdecl? props + 'and')
    1.23    ;
    1.24 +  decl: name ('::' type)? mixfix?
    1.25 +  ;
    1.26  \end{rail}
    1.27  
    1.28  \begin{descr}
     2.1 --- a/src/HOL/Library/State_Monad.thy	Wed Nov 29 23:33:09 2006 +0100
     2.2 +++ b/src/HOL/Library/State_Monad.thy	Thu Nov 30 14:17:22 2006 +0100
     2.3 @@ -256,7 +256,7 @@
     2.4  subsection {* Combinators *}
     2.5  
     2.6  definition
     2.7 -  lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c"
     2.8 +  lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c" where
     2.9    "lift f x = return (f x)"
    2.10  
    2.11  fun
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Nov 29 23:33:09 2006 +0100
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 30 14:17:22 2006 +0100
     3.3 @@ -188,32 +188,43 @@
     3.4        >> (Toplevel.theory o IsarCmd.add_defs));
     3.5  
     3.6  
     3.7 -(* constant definitions and abbreviations *)
     3.8 +(* old constdefs *)
     3.9  
    3.10 -val constdecl =
    3.11 -  (P.name --| P.$$$ "where") >> (fn x => (x, NONE, NoSyn)) ||
    3.12 -    P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
    3.13 -      --| Scan.option (P.$$$ "where") >> P.triple1 ||
    3.14 -    P.name -- (P.mixfix >> pair NONE) --| Scan.option (P.$$$ "where") >> P.triple2;
    3.15 +val old_constdecl =
    3.16 +  P.name --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
    3.17 +  P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
    3.18 +    --| Scan.option P.where_ >> P.triple1 ||
    3.19 +  P.name -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
    3.20  
    3.21 -val constdef = Scan.option constdecl -- (P.opt_thm_name ":" -- P.prop);
    3.22 +val old_constdef = Scan.option old_constdecl -- (P.opt_thm_name ":" -- P.prop);
    3.23  
    3.24  val structs =
    3.25    Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
    3.26  
    3.27  val constdefsP =
    3.28    OuterSyntax.command "constdefs" "old-style constant definition" K.thy_decl
    3.29 -    (structs -- Scan.repeat1 constdef >> (Toplevel.theory o Constdefs.add_constdefs));
    3.30 +    (structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
    3.31 +
    3.32 +
    3.33 +(* constant definitions and abbreviations *)
    3.34 +
    3.35 +val constdecl =
    3.36 +  P.name --
    3.37 +    (P.where_ >> K (NONE, NoSyn) ||
    3.38 +      P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
    3.39 +      Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
    3.40 +  >> P.triple2;
    3.41 +
    3.42 +val constdef = Scan.option constdecl -- (P.opt_thm_name ":" -- P.prop);
    3.43  
    3.44  val definitionP =
    3.45    OuterSyntax.command "definition" "constant definition" K.thy_decl
    3.46 -    (P.opt_locale_target -- Scan.repeat1 constdef
    3.47 +    (P.opt_locale_target -- (constdef >> single)
    3.48      >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args)));
    3.49  
    3.50  val abbreviationP =
    3.51    OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
    3.52 -    (P.opt_locale_target -- opt_mode --
    3.53 -      Scan.repeat1 (Scan.option constdecl -- P.prop)
    3.54 +    (P.opt_locale_target -- opt_mode -- (Scan.option constdecl -- P.prop >> single)
    3.55      >> (fn ((loc, mode), args) =>
    3.56          Toplevel.local_theory loc (Specification.abbreviation mode args)));
    3.57  
    3.58 @@ -230,7 +241,7 @@
    3.59    OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
    3.60      (P.opt_locale_target --
    3.61       (Scan.optional P.fixes [] --
    3.62 -      Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.spec)) [])
    3.63 +      Scan.optional (P.where_ |-- P.!!! (P.and_list1 P.spec)) [])
    3.64      >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y)));
    3.65  
    3.66  
    3.67 @@ -481,7 +492,7 @@
    3.68  val obtainP =
    3.69    OuterSyntax.command "obtain" "generalized existence"
    3.70      (K.tag_proof K.prf_asm_goal)
    3.71 -    (P.parname -- Scan.optional (P.fixes --| P.$$$ "where") [] -- P.statement
    3.72 +    (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- P.statement
    3.73        >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
    3.74  
    3.75  val guessP =