# HG changeset patch
# User wenzelm
# Date 1003170884 -7200
# Node ID d17ee22412577982859d1135368b9d3bcb38e2f8
# Parent  1aa328cb273a575155d5580f5e447912c2c46291
GPLed;

diff -r 1aa328cb273a -r d17ee2241257 src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Mon Oct 15 20:34:26 2001 +0200
+++ b/src/HOL/Library/List_Prefix.thy	Mon Oct 15 20:34:44 2001 +0200
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Library/List_Prefix.thy
     ID:         $Id$
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {*
diff -r 1aa328cb273a -r d17ee2241257 src/HOL/Library/Ring_and_Field.thy
--- a/src/HOL/Library/Ring_and_Field.thy	Mon Oct 15 20:34:26 2001 +0200
+++ b/src/HOL/Library/Ring_and_Field.thy	Mon Oct 15 20:34:44 2001 +0200
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Library/Ring_and_Field.thy
     ID:         $Id$
     Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {*