--- a/NEWS Mon Jun 06 16:04:26 2016 +0200
+++ b/NEWS Mon Jun 06 21:28:45 2016 +0200
@@ -108,6 +108,9 @@
*** HOL ***
+* Conventional syntax "%(). t" for unit abstractions. Slight syntactic
+INCOMPATIBILITY.
+
* Command 'code_reflect' accepts empty constructor lists for datatypes,
which renders those abstract effectively.
--- a/src/HOL/Product_Type.thy Mon Jun 06 16:04:26 2016 +0200
+++ b/src/HOL/Product_Type.thy Mon Jun 06 21:28:45 2016 +0200
@@ -305,6 +305,7 @@
"_pattern" :: "[pttrn, patterns] => pttrn" ("'(_,/ _')")
"" :: "pttrn => patterns" ("_")
"_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _")
+ "_unit" :: pttrn ("'(')")
translations
"(x, y)" \<rightleftharpoons> "CONST Pair x y"
@@ -317,6 +318,8 @@
\<comment> \<open>This rule accommodates tuples in \<open>case C \<dots> (x, y) \<dots> \<Rightarrow> \<dots>\<close>:
The \<open>(x, y)\<close> is parsed as \<open>Pair x y\<close> because it is \<open>logic\<close>,
not \<open>pttrn\<close>.\<close>
+ "\<lambda>(). b" \<rightleftharpoons> "CONST case_unit b"
+ "_abs (CONST Unity) t" \<rightharpoonup> "\<lambda>(). t"
text \<open>print @{term "case_prod f"} as @{term "\<lambda>(x, y). f x y"} and
@{term "case_prod (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close>