# HG changeset patch
# User blanchet
# Date 1391004353 -3600
# Node ID 2d69438b1b0cb6ce8472e409f1fb28b9ce73ef53
# Parent  608c157d743dee1871a48d28cc9c85a851d1e292
added Dmitriy, since he did the case syntax

diff -r 608c157d743d -r 2d69438b1b0c src/HOL/Ctr_Sugar.thy
--- a/src/HOL/Ctr_Sugar.thy	Wed Jan 29 12:51:37 2014 +0000
+++ b/src/HOL/Ctr_Sugar.thy	Wed Jan 29 15:05:53 2014 +0100
@@ -1,5 +1,6 @@
 (*  Title:      HOL/Ctr_Sugar.thy
     Author:     Jasmin Blanchette, TU Muenchen
+    Author:     Dmitriy Traytel, TU Muenchen
     Copyright   2012, 2013
 
 Wrapping existing freely generated type's constructors.