# HG changeset patch
# User wenzelm
# Date 1012240308 -3600
# Node ID 6214f03d6d27118d53d5b162bf682030247d606c
# Parent  a4386cc9b1c3d01dc7ca55ed36e53a1770bd5807
GPLed;

diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/Basis.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Basis.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 *)
 header {* Definitions extending HOL as logical basis of Bali *}
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/Conform.thy
--- a/src/HOL/Bali/Conform.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/Conform.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Conform.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {* Conformance notions for the type soundness proof for Java *}
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/Decl.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Decl.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 header {* Field, method, interface, and class declarations, whole Java programs
 *}
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/Eval.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Eval.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 header {* Operational evaluation (big-step) semantics of Java expressions and 
           statements
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/Example.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Example.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 header {* Example Bali program *}
 
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/Name.thy
--- a/src/HOL/Bali/Name.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/Name.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Name.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 header {* Java names *}
 
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/State.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/State.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 header {* State for evaluation of Java expressions and statements *}
 
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/Table.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Table.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 header {* Abstract tables and their implementation as lists *}
 
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/Term.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Term.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {* Java expressions and statements *}
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/Trans.thy
--- a/src/HOL/Bali/Trans.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/Trans.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Trans.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Operational transition (small-step) semantics of the 
 execution of Java expressions and statements
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/Type.thy
--- a/src/HOL/Bali/Type.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/Type.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Type.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {* Java types *}
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/TypeRel.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/TypeRel.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 header {* The relations between Java types *}
 
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/TypeSafe.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/TypeSafe.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 header {* The type soundness proof for Java *}
 
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/Value.thy
--- a/src/HOL/Bali/Value.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/Value.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/Value.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 header {* Java values *}
 
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/WellForm.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/WellForm.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
 header {* Well-formedness of Java programs *}
diff -r a4386cc9b1c3 -r 6214f03d6d27 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Mon Jan 28 18:50:23 2002 +0100
+++ b/src/HOL/Bali/WellType.thy	Mon Jan 28 18:51:48 2002 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Bali/WellType.thy
     ID:         $Id$
     Author:     David von Oheimb
-    Copyright   1997 Technische Universitaet Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 header {* Well-typedness of Java programs *}