GPLed;
authorwenzelm
Mon Jan 28 18:51:48 2002 +0100 (2002-01-28)
changeset 128586214f03d6d27
parent 12857 a4386cc9b1c3
child 12859 f63315dfffd4
GPLed;
src/HOL/Bali/Basis.thy
src/HOL/Bali/Conform.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/Name.thy
src/HOL/Bali/State.thy
src/HOL/Bali/Table.thy
src/HOL/Bali/Term.thy
src/HOL/Bali/Trans.thy
src/HOL/Bali/Type.thy
src/HOL/Bali/TypeRel.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Bali/Value.thy
src/HOL/Bali/WellForm.thy
src/HOL/Bali/WellType.thy
     1.1 --- a/src/HOL/Bali/Basis.thy	Mon Jan 28 18:50:23 2002 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Mon Jan 28 18:51:48 2002 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOL/Bali/Basis.thy
     1.5      ID:         $Id$
     1.6      Author:     David von Oheimb
     1.7 -    Copyright   1997 Technische Universitaet Muenchen
     1.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  
    1.10  *)
    1.11  header {* Definitions extending HOL as logical basis of Bali *}
     2.1 --- a/src/HOL/Bali/Conform.thy	Mon Jan 28 18:50:23 2002 +0100
     2.2 +++ b/src/HOL/Bali/Conform.thy	Mon Jan 28 18:51:48 2002 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  (*  Title:      HOL/Bali/Conform.thy
     2.5      ID:         $Id$
     2.6      Author:     David von Oheimb
     2.7 -    Copyright   1997 Technische Universitaet Muenchen
     2.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.9  *)
    2.10  
    2.11  header {* Conformance notions for the type soundness proof for Java *}
     3.1 --- a/src/HOL/Bali/Decl.thy	Mon Jan 28 18:50:23 2002 +0100
     3.2 +++ b/src/HOL/Bali/Decl.thy	Mon Jan 28 18:51:48 2002 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  (*  Title:      HOL/Bali/Decl.thy
     3.5      ID:         $Id$
     3.6      Author:     David von Oheimb
     3.7 -    Copyright   1997 Technische Universitaet Muenchen
     3.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.9  *)
    3.10  header {* Field, method, interface, and class declarations, whole Java programs
    3.11  *}
     4.1 --- a/src/HOL/Bali/Eval.thy	Mon Jan 28 18:50:23 2002 +0100
     4.2 +++ b/src/HOL/Bali/Eval.thy	Mon Jan 28 18:51:48 2002 +0100
     4.3 @@ -1,7 +1,7 @@
     4.4  (*  Title:      HOL/Bali/Eval.thy
     4.5      ID:         $Id$
     4.6      Author:     David von Oheimb
     4.7 -    Copyright   1997 Technische Universitaet Muenchen
     4.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4.9  *)
    4.10  header {* Operational evaluation (big-step) semantics of Java expressions and 
    4.11            statements
     5.1 --- a/src/HOL/Bali/Example.thy	Mon Jan 28 18:50:23 2002 +0100
     5.2 +++ b/src/HOL/Bali/Example.thy	Mon Jan 28 18:51:48 2002 +0100
     5.3 @@ -1,7 +1,7 @@
     5.4  (*  Title:      HOL/Bali/Example.thy
     5.5      ID:         $Id$
     5.6      Author:     David von Oheimb
     5.7 -    Copyright   1997 Technische Universitaet Muenchen
     5.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5.9  *)
    5.10  header {* Example Bali program *}
    5.11  
     6.1 --- a/src/HOL/Bali/Name.thy	Mon Jan 28 18:50:23 2002 +0100
     6.2 +++ b/src/HOL/Bali/Name.thy	Mon Jan 28 18:51:48 2002 +0100
     6.3 @@ -1,7 +1,7 @@
     6.4  (*  Title:      HOL/Bali/Name.thy
     6.5      ID:         $Id$
     6.6      Author:     David von Oheimb
     6.7 -    Copyright   1997 Technische Universitaet Muenchen
     6.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     6.9  *)
    6.10  header {* Java names *}
    6.11  
     7.1 --- a/src/HOL/Bali/State.thy	Mon Jan 28 18:50:23 2002 +0100
     7.2 +++ b/src/HOL/Bali/State.thy	Mon Jan 28 18:51:48 2002 +0100
     7.3 @@ -1,7 +1,7 @@
     7.4  (*  Title:      HOL/Bali/State.thy
     7.5      ID:         $Id$
     7.6      Author:     David von Oheimb
     7.7 -    Copyright   1997 Technische Universitaet Muenchen
     7.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     7.9  *)
    7.10  header {* State for evaluation of Java expressions and statements *}
    7.11  
     8.1 --- a/src/HOL/Bali/Table.thy	Mon Jan 28 18:50:23 2002 +0100
     8.2 +++ b/src/HOL/Bali/Table.thy	Mon Jan 28 18:51:48 2002 +0100
     8.3 @@ -1,7 +1,7 @@
     8.4  (*  Title:      HOL/Bali/Table.thy
     8.5      ID:         $Id$
     8.6      Author:     David von Oheimb
     8.7 -    Copyright   1997 Technische Universitaet Muenchen
     8.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     8.9  *)
    8.10  header {* Abstract tables and their implementation as lists *}
    8.11  
     9.1 --- a/src/HOL/Bali/Term.thy	Mon Jan 28 18:50:23 2002 +0100
     9.2 +++ b/src/HOL/Bali/Term.thy	Mon Jan 28 18:51:48 2002 +0100
     9.3 @@ -1,7 +1,7 @@
     9.4  (*  Title:      HOL/Bali/Term.thy
     9.5      ID:         $Id$
     9.6      Author:     David von Oheimb
     9.7 -    Copyright   1997 Technische Universitaet Muenchen
     9.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     9.9  *)
    9.10  
    9.11  header {* Java expressions and statements *}
    10.1 --- a/src/HOL/Bali/Trans.thy	Mon Jan 28 18:50:23 2002 +0100
    10.2 +++ b/src/HOL/Bali/Trans.thy	Mon Jan 28 18:51:48 2002 +0100
    10.3 @@ -1,7 +1,7 @@
    10.4  (*  Title:      HOL/Bali/Trans.thy
    10.5      ID:         $Id$
    10.6      Author:     David von Oheimb
    10.7 -    Copyright   1997 Technische Universitaet Muenchen
    10.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    10.9  
   10.10  Operational transition (small-step) semantics of the 
   10.11  execution of Java expressions and statements
    11.1 --- a/src/HOL/Bali/Type.thy	Mon Jan 28 18:50:23 2002 +0100
    11.2 +++ b/src/HOL/Bali/Type.thy	Mon Jan 28 18:51:48 2002 +0100
    11.3 @@ -1,7 +1,7 @@
    11.4  (*  Title:      HOL/Bali/Type.thy
    11.5      ID:         $Id$
    11.6      Author:     David von Oheimb
    11.7 -    Copyright   1997 Technische Universitaet Muenchen
    11.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    11.9  *)
   11.10  
   11.11  header {* Java types *}
    12.1 --- a/src/HOL/Bali/TypeRel.thy	Mon Jan 28 18:50:23 2002 +0100
    12.2 +++ b/src/HOL/Bali/TypeRel.thy	Mon Jan 28 18:51:48 2002 +0100
    12.3 @@ -1,7 +1,7 @@
    12.4  (*  Title:      HOL/Bali/TypeRel.thy
    12.5      ID:         $Id$
    12.6      Author:     David von Oheimb
    12.7 -    Copyright   1997 Technische Universitaet Muenchen
    12.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    12.9  *)
   12.10  header {* The relations between Java types *}
   12.11  
    13.1 --- a/src/HOL/Bali/TypeSafe.thy	Mon Jan 28 18:50:23 2002 +0100
    13.2 +++ b/src/HOL/Bali/TypeSafe.thy	Mon Jan 28 18:51:48 2002 +0100
    13.3 @@ -1,7 +1,7 @@
    13.4  (*  Title:      HOL/Bali/TypeSafe.thy
    13.5      ID:         $Id$
    13.6      Author:     David von Oheimb
    13.7 -    Copyright   1997 Technische Universitaet Muenchen
    13.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    13.9  *)
   13.10  header {* The type soundness proof for Java *}
   13.11  
    14.1 --- a/src/HOL/Bali/Value.thy	Mon Jan 28 18:50:23 2002 +0100
    14.2 +++ b/src/HOL/Bali/Value.thy	Mon Jan 28 18:51:48 2002 +0100
    14.3 @@ -1,7 +1,7 @@
    14.4  (*  Title:      HOL/Bali/Value.thy
    14.5      ID:         $Id$
    14.6      Author:     David von Oheimb
    14.7 -    Copyright   1997 Technische Universitaet Muenchen
    14.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    14.9  *)
   14.10  header {* Java values *}
   14.11  
    15.1 --- a/src/HOL/Bali/WellForm.thy	Mon Jan 28 18:50:23 2002 +0100
    15.2 +++ b/src/HOL/Bali/WellForm.thy	Mon Jan 28 18:51:48 2002 +0100
    15.3 @@ -1,7 +1,7 @@
    15.4  (*  Title:      HOL/Bali/WellForm.thy
    15.5      ID:         $Id$
    15.6      Author:     David von Oheimb
    15.7 -    Copyright   1997 Technische Universitaet Muenchen
    15.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    15.9  *)
   15.10  
   15.11  header {* Well-formedness of Java programs *}
    16.1 --- a/src/HOL/Bali/WellType.thy	Mon Jan 28 18:50:23 2002 +0100
    16.2 +++ b/src/HOL/Bali/WellType.thy	Mon Jan 28 18:51:48 2002 +0100
    16.3 @@ -1,7 +1,7 @@
    16.4  (*  Title:      HOL/Bali/WellType.thy
    16.5      ID:         $Id$
    16.6      Author:     David von Oheimb
    16.7 -    Copyright   1997 Technische Universitaet Muenchen
    16.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    16.9  *)
   16.10  header {* Well-typedness of Java programs *}
   16.11