# HG changeset patch
# User wenzelm
# Date 1472758135 -7200
# Node ID f3ad26c4b2d9e3f18c6a36e22d463fe79b05380c
# Parent  0f61ea70d3843932aa8fe3d044bb20fbad99dfa9
tuned headers;

diff -r 0f61ea70d384 -r f3ad26c4b2d9 src/HOL/Library/Polynomial_Factorial.thy
--- a/src/HOL/Library/Polynomial_Factorial.thy	Thu Sep 01 21:28:46 2016 +0200
+++ b/src/HOL/Library/Polynomial_Factorial.thy	Thu Sep 01 21:28:55 2016 +0200
@@ -1,3 +1,11 @@
+(*  Title:      HOL/Library/Polynomial_Factorial.thy
+    Author:     Brian Huffman
+    Author:     Clemens Ballarin
+    Author:     Amine Chaieb
+    Author:     Florian Haftmann
+    Author:     Manuel Eberl
+*)
+
 theory Polynomial_Factorial
 imports 
   Complex_Main
@@ -1470,4 +1478,4 @@
   
 value [code] "Lcm {[:1,2,3:], [:2,3,4::int poly:]}"
 
-end
\ No newline at end of file
+end
diff -r 0f61ea70d384 -r f3ad26c4b2d9 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Sep 01 21:28:46 2016 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Sep 01 21:28:55 2016 +0200
@@ -1,5 +1,9 @@
+(*  Title:      HOL/Library/Predicate_Compile_Alternative_Defs.thy
+    Author:     Lukas Bulwahn, TU Muenchen
+*)
+
 theory Predicate_Compile_Alternative_Defs
-imports Main
+  imports Main
 begin
 
 section \<open>Common constants\<close>
diff -r 0f61ea70d384 -r f3ad26c4b2d9 src/HOL/Library/Predicate_Compile_Quickcheck.thy
--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Thu Sep 01 21:28:46 2016 +0200
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Thu Sep 01 21:28:55 2016 +0200
@@ -1,9 +1,11 @@
-(* Author: Lukas Bulwahn, TU Muenchen *)
+(*  Title:      HOL/Library/Predicate_Compile_Alternative_Defs.thy
+    Author:     Lukas Bulwahn, TU Muenchen
+*)
 
 section \<open>A Prototype of Quickcheck based on the Predicate Compiler\<close>
 
 theory Predicate_Compile_Quickcheck
-imports Main Predicate_Compile_Alternative_Defs
+  imports Predicate_Compile_Alternative_Defs
 begin
 
 ML_file "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"