1.1 --- a/src/HOLCF/Adm.thy Wed May 25 09:04:24 2005 +0200
1.2 +++ b/src/HOLCF/Adm.thy Wed May 25 09:44:34 2005 +0200
1.3 @@ -1,7 +1,6 @@
1.4 (* Title: HOLCF/Adm.thy
1.5 ID: $Id$
1.6 Author: Franz Regensburger
1.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
1.8 *)
1.9
1.10 header {* Admissibility *}
2.1 --- a/src/HOLCF/Cfun.thy Wed May 25 09:04:24 2005 +0200
2.2 +++ b/src/HOLCF/Cfun.thy Wed May 25 09:44:34 2005 +0200
2.3 @@ -1,10 +1,8 @@
2.4 (* Title: HOLCF/Cfun.thy
2.5 ID: $Id$
2.6 Author: Franz Regensburger
2.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
2.8
2.9 Definition of the type -> of continuous functions.
2.10 -
2.11 *)
2.12
2.13 header {* The type of continuous functions *}
3.1 --- a/src/HOLCF/Cont.thy Wed May 25 09:04:24 2005 +0200
3.2 +++ b/src/HOLCF/Cont.thy Wed May 25 09:44:34 2005 +0200
3.3 @@ -1,9 +1,8 @@
3.4 (* Title: HOLCF/Cont.thy
3.5 ID: $Id$
3.6 Author: Franz Regensburger
3.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
3.8
3.9 - Results about continuity and monotonicity
3.10 +Results about continuity and monotonicity.
3.11 *)
3.12
3.13 header {* Continuity and monotonicity *}
4.1 --- a/src/HOLCF/Cprod.thy Wed May 25 09:04:24 2005 +0200
4.2 +++ b/src/HOLCF/Cprod.thy Wed May 25 09:44:34 2005 +0200
4.3 @@ -1,9 +1,8 @@
4.4 (* Title: HOLCF/Cprod.thy
4.5 ID: $Id$
4.6 Author: Franz Regensburger
4.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
4.8
4.9 -Partial ordering for cartesian product of HOL theory prod.thy
4.10 +Partial ordering for cartesian product of HOL products.
4.11 *)
4.12
4.13 header {* The cpo of cartesian products *}
5.1 --- a/src/HOLCF/Discrete.thy Wed May 25 09:04:24 2005 +0200
5.2 +++ b/src/HOLCF/Discrete.thy Wed May 25 09:44:34 2005 +0200
5.3 @@ -1,7 +1,6 @@
5.4 (* Title: HOLCF/Discrete.thy
5.5 ID: $Id$
5.6 Author: Tobias Nipkow
5.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
5.8
5.9 Discrete CPOs.
5.10 *)
6.1 --- a/src/HOLCF/Domain.thy Wed May 25 09:04:24 2005 +0200
6.2 +++ b/src/HOLCF/Domain.thy Wed May 25 09:44:34 2005 +0200
6.3 @@ -1,7 +1,6 @@
6.4 (* Title: HOLCF/Domain.thy
6.5 ID: $Id$
6.6 Author: Brian Huffman
6.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
6.8 *)
6.9
6.10 header {* Domain package *}
7.1 --- a/src/HOLCF/Fix.thy Wed May 25 09:04:24 2005 +0200
7.2 +++ b/src/HOLCF/Fix.thy Wed May 25 09:44:34 2005 +0200
7.3 @@ -1,9 +1,8 @@
7.4 (* Title: HOLCF/Fix.thy
7.5 ID: $Id$
7.6 Author: Franz Regensburger
7.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
7.8
7.9 -definitions for fixed point operator and admissibility
7.10 +Definitions for fixed point operator and admissibility.
7.11 *)
7.12
7.13 header {* Fixed point operator and admissibility *}
8.1 --- a/src/HOLCF/FunCpo.thy Wed May 25 09:04:24 2005 +0200
8.2 +++ b/src/HOLCF/FunCpo.thy Wed May 25 09:44:34 2005 +0200
8.3 @@ -1,13 +1,12 @@
8.4 (* Title: HOLCF/FunCpo.thy
8.5 ID: $Id$
8.6 Author: Franz Regensburger
8.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
8.8
8.9 Definition of the partial ordering for the type of all functions => (fun)
8.10
8.11 REMARK: The ordering on 'a => 'b is only defined if 'b is in class po !!
8.12
8.13 -Class instance of => (fun) for class pcpo
8.14 +Class instance of => (fun) for class pcpo.
8.15 *)
8.16
8.17 header {* Class instances for the type of all functions *}
9.1 --- a/src/HOLCF/One.thy Wed May 25 09:04:24 2005 +0200
9.2 +++ b/src/HOLCF/One.thy Wed May 25 09:44:34 2005 +0200
9.3 @@ -1,7 +1,8 @@
9.4 (* Title: HOLCF/One.thy
9.5 ID: $Id$
9.6 Author: Oscar Slotosch
9.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
9.8 +
9.9 +The unit domain.
9.10 *)
9.11
9.12 header {* The unit domain *}
9.13 @@ -19,14 +20,6 @@
9.14 translations
9.15 "one" <= (type) "unit lift"
9.16
9.17 -(* Title: HOLCF/One.ML
9.18 - ID: $Id$
9.19 - Author: Oscar Slotosch
9.20 - License: GPL (GNU GENERAL PUBLIC LICENSE)
9.21 -
9.22 -The unit domain.
9.23 -*)
9.24 -
9.25 (* ------------------------------------------------------------------------ *)
9.26 (* Exhaustion and Elimination for type one *)
9.27 (* ------------------------------------------------------------------------ *)
10.1 --- a/src/HOLCF/Pcpo.thy Wed May 25 09:04:24 2005 +0200
10.2 +++ b/src/HOLCF/Pcpo.thy Wed May 25 09:44:34 2005 +0200
10.3 @@ -1,9 +1,8 @@
10.4 (* Title: HOLCF/Pcpo.thy
10.5 ID: $Id$
10.6 Author: Franz Regensburger
10.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
10.8
10.9 -introduction of the classes cpo and pcpo
10.10 +Introduction of the classes cpo and pcpo.
10.11 *)
10.12
10.13 header {* Classes cpo and pcpo *}
11.1 --- a/src/HOLCF/Porder.thy Wed May 25 09:04:24 2005 +0200
11.2 +++ b/src/HOLCF/Porder.thy Wed May 25 09:44:34 2005 +0200
11.3 @@ -1,10 +1,9 @@
11.4 (* Title: HOLCF/Porder.thy
11.5 ID: $Id$
11.6 Author: Franz Regensburger
11.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
11.8
11.9 Definition of class porder (partial order).
11.10 -Conservative extension of theory Porder0 by constant definitions
11.11 +Conservative extension of theory Porder0 by constant definitions.
11.12 *)
11.13
11.14 header {* Partial orders *}
12.1 --- a/src/HOLCF/Sprod.thy Wed May 25 09:04:24 2005 +0200
12.2 +++ b/src/HOLCF/Sprod.thy Wed May 25 09:44:34 2005 +0200
12.3 @@ -1,7 +1,6 @@
12.4 (* Title: HOLCF/Sprod.thy
12.5 ID: $Id$
12.6 Author: Franz Regensburger and Brian Huffman
12.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
12.8
12.9 Strict product with typedef.
12.10 *)
13.1 --- a/src/HOLCF/Ssum.thy Wed May 25 09:04:24 2005 +0200
13.2 +++ b/src/HOLCF/Ssum.thy Wed May 25 09:44:34 2005 +0200
13.3 @@ -1,9 +1,8 @@
13.4 (* Title: HOLCF/Ssum.thy
13.5 ID: $Id$
13.6 Author: Franz Regensburger and Brian Huffman
13.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
13.8
13.9 -Strict sum with typedef
13.10 +Strict sum with typedef.
13.11 *)
13.12
13.13 header {* The type of strict sums *}
14.1 --- a/src/HOLCF/Tr.thy Wed May 25 09:04:24 2005 +0200
14.2 +++ b/src/HOLCF/Tr.thy Wed May 25 09:44:34 2005 +0200
14.3 @@ -1,9 +1,8 @@
14.4 (* Title: HOLCF/Tr.thy
14.5 ID: $Id$
14.6 Author: Franz Regensburger
14.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
14.8
14.9 -Introduce infix if_then_else_fi and boolean connectives andalso, orelse
14.10 +Introduce infix if_then_else_fi and boolean connectives andalso, orelse.
14.11 *)
14.12
14.13 header {* The type of lifted booleans *}
15.1 --- a/src/HOLCF/TypedefPcpo.thy Wed May 25 09:04:24 2005 +0200
15.2 +++ b/src/HOLCF/TypedefPcpo.thy Wed May 25 09:44:34 2005 +0200
15.3 @@ -1,7 +1,6 @@
15.4 (* Title: HOLCF/TypedefPcpo.thy
15.5 ID: $Id$
15.6 Author: Brian Huffman
15.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
15.8 *)
15.9
15.10 header {* Subtypes of pcpos *}
16.1 --- a/src/HOLCF/Up.thy Wed May 25 09:04:24 2005 +0200
16.2 +++ b/src/HOLCF/Up.thy Wed May 25 09:44:34 2005 +0200
16.3 @@ -1,8 +1,6 @@
16.4 (* Title: HOLCF/Up.thy
16.5 ID: $Id$
16.6 - Author: Franz Regensburger
16.7 - Additions by Brian Huffman
16.8 - License: GPL (GNU GENERAL PUBLIC LICENSE)
16.9 + Author: Franz Regensburger and Brian Huffman
16.10
16.11 Lifting.
16.12 *)
17.1 --- a/src/HOLCF/domain/extender.ML Wed May 25 09:04:24 2005 +0200
17.2 +++ b/src/HOLCF/domain/extender.ML Wed May 25 09:44:34 2005 +0200
17.3 @@ -1,7 +1,6 @@
17.4 (* Title: HOLCF/domain/extender.ML
17.5 ID: $Id$
17.6 Author: David von Oheimb
17.7 - License: GPL (GNU GENERAL PUBLIC LICENSE)
17.8
17.9 Theory extender for domain section, including new-style theory syntax.
17.10