# 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 \ 'b) \ 'a \ 'c \ 'b \ 'c" + lift :: "('a \ 'b) \ 'a \ 'c \ 'b \ '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 =