# HG changeset patch # User blanchet # Date 1406669975 -7200 # Node ID afef6616cbae35c3ff48a3c2ef91d7afe05065bf # Parent 44341963ade3496f4f5a832c2790909c07bb5dc9 header tuning diff -r 44341963ade3 -r afef6616cbae src/HOL/BNF_Comp.thy --- a/src/HOL/BNF_Comp.thy Mon Jul 28 10:57:33 2014 +0200 +++ b/src/HOL/BNF_Comp.thy Tue Jul 29 23:39:35 2014 +0200 @@ -1,6 +1,7 @@ (* Title: HOL/BNF_Comp.thy Author: Dmitriy Traytel, TU Muenchen - Copyright 2012 + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012, 2013, 2014 Composition of bounded natural functors. *) diff -r 44341963ade3 -r afef6616cbae src/HOL/BNF_Def.thy --- a/src/HOL/BNF_Def.thy Mon Jul 28 10:57:33 2014 +0200 +++ b/src/HOL/BNF_Def.thy Tue Jul 29 23:39:35 2014 +0200 @@ -1,7 +1,7 @@ (* Title: HOL/BNF_Def.thy Author: Dmitriy Traytel, TU Muenchen Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 + Copyright 2012, 2013, 2014 Definition of bounded natural functors. *) diff -r 44341963ade3 -r afef6616cbae src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Mon Jul 28 10:57:33 2014 +0200 +++ b/src/HOL/BNF_FP_Base.thy Tue Jul 29 23:39:35 2014 +0200 @@ -2,7 +2,8 @@ Author: Lorenz Panny, TU Muenchen Author: Dmitriy Traytel, TU Muenchen Author: Jasmin Blanchette, TU Muenchen - Copyright 2012, 2013 + Author: Martin Desharnais, TU Muenchen + Copyright 2012, 2013, 2014 Shared fixed point operations on bounded natural functors. *) diff -r 44341963ade3 -r afef6616cbae src/HOL/BNF_GFP.thy --- a/src/HOL/BNF_GFP.thy Mon Jul 28 10:57:33 2014 +0200 +++ b/src/HOL/BNF_GFP.thy Tue Jul 29 23:39:35 2014 +0200 @@ -2,7 +2,7 @@ Author: Dmitriy Traytel, TU Muenchen Author: Lorenz Panny, TU Muenchen Author: Jasmin Blanchette, TU Muenchen - Copyright 2012, 2013 + Copyright 2012, 2013, 2014 Greatest fixed point operation on bounded natural functors. *) diff -r 44341963ade3 -r afef6616cbae src/HOL/BNF_LFP.thy --- a/src/HOL/BNF_LFP.thy Mon Jul 28 10:57:33 2014 +0200 +++ b/src/HOL/BNF_LFP.thy Tue Jul 29 23:39:35 2014 +0200 @@ -1,9 +1,8 @@ - (* Title: HOL/BNF_LFP.thy Author: Dmitriy Traytel, TU Muenchen Author: Lorenz Panny, TU Muenchen Author: Jasmin Blanchette, TU Muenchen - Copyright 2012, 2013 + Copyright 2012, 2013, 2014 Least fixed point operation on bounded natural functors. *)