# HG changeset patch # User blanchet # Date 1384260444 -3600 # Node ID f4b4fa25ce567bd2ba626e75cf3cf6ac858067ee # Parent 8baee6b04a7cf0e5fa75b4fba22ab33e737f92cd tuned headers diff -r 8baee6b04a7c -r f4b4fa25ce56 src/HOL/Ctr_Sugar.thy --- a/src/HOL/Ctr_Sugar.thy Tue Nov 12 13:47:24 2013 +0100 +++ b/src/HOL/Ctr_Sugar.thy Tue Nov 12 13:47:24 2013 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/BNF/Ctr_Sugar.thy +(* Title: HOL/Ctr_Sugar.thy Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 + Copyright 2012, 2013 Wrapping existing freely generated type's constructors. *) diff -r 8baee6b04a7c -r f4b4fa25ce56 src/HOL/Tools/ctr_sugar.ML --- a/src/HOL/Tools/ctr_sugar.ML Tue Nov 12 13:47:24 2013 +0100 +++ b/src/HOL/Tools/ctr_sugar.ML Tue Nov 12 13:47:24 2013 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/BNF/Tools/ctr_sugar.ML +(* Title: HOL/Tools/ctr_sugar.ML Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 + Copyright 2012, 2013 Wrapping existing freely generated type's constructors. *) diff -r 8baee6b04a7c -r f4b4fa25ce56 src/HOL/Tools/ctr_sugar_tactics.ML --- a/src/HOL/Tools/ctr_sugar_tactics.ML Tue Nov 12 13:47:24 2013 +0100 +++ b/src/HOL/Tools/ctr_sugar_tactics.ML Tue Nov 12 13:47:24 2013 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/BNF/Tools/ctr_sugar_tactics.ML +(* Title: HOL/Tools/ctr_sugar_tactics.ML Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 + Copyright 2012, 2013 Tactics for wrapping existing freely generated type's constructors. *) diff -r 8baee6b04a7c -r f4b4fa25ce56 src/HOL/Tools/ctr_sugar_util.ML --- a/src/HOL/Tools/ctr_sugar_util.ML Tue Nov 12 13:47:24 2013 +0100 +++ b/src/HOL/Tools/ctr_sugar_util.ML Tue Nov 12 13:47:24 2013 +0100 @@ -1,6 +1,7 @@ -(* Title: HOL/BNF/Tools/ctr_sugar_util.ML +(* Title: HOL/Tools/ctr_sugar_util.ML + Author: Dmitriy Traytel, TU Muenchen Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 + Copyright 2012, 2013 Library for wrapping existing freely generated type's constructors. *)