--- 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 *}
--- 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 *}
--- 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
*}
--- 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
--- 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 *}
--- 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 *}
--- 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 *}
--- 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 *}
--- 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 *}
--- 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
--- 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 *}
--- 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 *}
--- 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 *}
--- 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 *}
--- 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 *}
--- 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 *}