--- a/src/HOL/AxClasses/Group.thy Fri Dec 15 17:59:30 2000 +0100
+++ b/src/HOL/AxClasses/Group.thy Fri Dec 15 17:59:45 2000 +0100
@@ -1,6 +1,7 @@
(* Title: HOL/AxClasses/Group.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
theory Group = Main:
--- a/src/HOL/AxClasses/Product.thy Fri Dec 15 17:59:30 2000 +0100
+++ b/src/HOL/AxClasses/Product.thy Fri Dec 15 17:59:45 2000 +0100
@@ -1,6 +1,7 @@
(* Title: HOL/AxClasses/Product.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
theory Product = Main:
--- a/src/HOL/AxClasses/Semigroups.thy Fri Dec 15 17:59:30 2000 +0100
+++ b/src/HOL/AxClasses/Semigroups.thy Fri Dec 15 17:59:45 2000 +0100
@@ -1,6 +1,7 @@
(* Title: HOL/AxClasses/Semigroups.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
theory Semigroups = Main:
--- a/src/HOL/Library/Quotient.thy Fri Dec 15 17:59:30 2000 +0100
+++ b/src/HOL/Library/Quotient.thy Fri Dec 15 17:59:45 2000 +0100
@@ -1,6 +1,7 @@
(* Title: HOL/Library/Quotient.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {*
--- a/src/HOL/Library/Rational_Numbers.thy Fri Dec 15 17:59:30 2000 +0100
+++ b/src/HOL/Library/Rational_Numbers.thy Fri Dec 15 17:59:45 2000 +0100
@@ -1,3 +1,8 @@
+(* Title: HOL/Library/Rational_Numbers.thy
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+*)
header {*
\title{Rational numbers}