Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Function/partial_function.ML
changeset 46949 94aa7b81bcf6
parent 45403 7a0b8debef77
child 46961 5c6955f487e5 
--- a/src/HOL/Tools/Function/partial_function.ML	Thu Mar 15 19:48:19 2012 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Thu Mar 15 20:07:00 2012 +0100
@@ -279,7 +279,7 @@
 val add_partial_function = gen_add_partial_function Specification.check_spec;
 val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
 
-val mode = Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")";
+val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
 
 val _ = Outer_Syntax.local_theory
   "partial_function" "define partial function" Keyword.thy_decl
isabelle