# HG changeset patch
# User haftmann
# Date 1465241325 -7200
# Node ID 3e908f762817eaec543104b48ffbee781a04fd38
# Parent  48bc9045866e547236447530968ba3695a459d0a
conventional syntax for unit abstractions

diff -r 48bc9045866e -r 3e908f762817 NEWS
--- 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.
 
diff -r 48bc9045866e -r 3e908f762817 src/HOL/Product_Type.thy
--- 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>