# 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)" \ "CONST Pair x y" @@ -317,6 +318,8 @@ \ \This rule accommodates tuples in \case C \ (x, y) \ \ \\: The \(x, y)\ is parsed as \Pair x y\ because it is \logic\, not \pttrn\.\ + "\(). b" \ "CONST case_unit b" + "_abs (CONST Unity) t" \ "\(). t" text \print @{term "case_prod f"} as @{term "\(x, y). f x y"} and @{term "case_prod (\x. f x)"} as @{term "\(x, y). f x y"}\