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