GPLed;
authorwenzelm
Sat Nov 03 01:41:26 2001 +0100 (2001-11-03)
changeset 1203046d57d0290a2
parent 12029 7df1d840d01d
child 12031 1b883fa9458e
GPLed;
src/HOLCF/Cfun1.ML
src/HOLCF/Cfun1.thy
src/HOLCF/Cfun2.ML
src/HOLCF/Cfun2.thy
src/HOLCF/Cfun3.ML
src/HOLCF/Cfun3.thy
src/HOLCF/Cont.ML
src/HOLCF/Cont.thy
src/HOLCF/Cprod1.ML
src/HOLCF/Cprod1.thy
src/HOLCF/Cprod2.ML
src/HOLCF/Cprod2.thy
src/HOLCF/Cprod3.ML
src/HOLCF/Cprod3.thy
src/HOLCF/Discrete.ML
src/HOLCF/Discrete.thy
src/HOLCF/Discrete0.ML
src/HOLCF/Discrete0.thy
src/HOLCF/Discrete1.ML
src/HOLCF/Discrete1.thy
src/HOLCF/Fix.ML
src/HOLCF/Fix.thy
src/HOLCF/Fun1.ML
src/HOLCF/Fun1.thy
src/HOLCF/Fun2.ML
src/HOLCF/Fun2.thy
src/HOLCF/Fun3.ML
src/HOLCF/Fun3.thy
src/HOLCF/HOLCF.ML
src/HOLCF/HOLCF.thy
src/HOLCF/One.ML
src/HOLCF/One.thy
src/HOLCF/Pcpo.ML
src/HOLCF/Pcpo.thy
src/HOLCF/Porder.ML
src/HOLCF/Porder.thy
src/HOLCF/Porder0.ML
src/HOLCF/Porder0.thy
src/HOLCF/Sprod0.ML
src/HOLCF/Sprod0.thy
src/HOLCF/Sprod1.ML
src/HOLCF/Sprod1.thy
src/HOLCF/Sprod2.ML
src/HOLCF/Sprod2.thy
src/HOLCF/Sprod3.ML
src/HOLCF/Sprod3.thy
src/HOLCF/Ssum0.ML
src/HOLCF/Ssum0.thy
src/HOLCF/Ssum1.ML
src/HOLCF/Ssum1.thy
src/HOLCF/Ssum2.ML
src/HOLCF/Ssum2.thy
src/HOLCF/Ssum3.ML
src/HOLCF/Ssum3.thy
src/HOLCF/Tr.ML
src/HOLCF/Tr.thy
src/HOLCF/Up1.ML
src/HOLCF/Up1.thy
src/HOLCF/Up2.ML
src/HOLCF/Up2.thy
src/HOLCF/Up3.ML
src/HOLCF/Up3.thy
src/HOLCF/cont_consts.ML
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/extender.ML
src/HOLCF/domain/interface.ML
src/HOLCF/domain/library.ML
src/HOLCF/domain/syntax.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/holcf_logic.ML
     1.1 --- a/src/HOLCF/Cfun1.ML	Sat Nov 03 01:40:28 2001 +0100
     1.2 +++ b/src/HOLCF/Cfun1.ML	Sat Nov 03 01:41:26 2001 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOLCF/Cfun1.ML
     1.5      ID:         $Id$
     1.6      Author:     Franz Regensburger
     1.7 -    Copyright   1993 Technische Universitaet Muenchen
     1.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  
    1.10  The type ->  of continuous functions.
    1.11  *)
     2.1 --- a/src/HOLCF/Cfun1.thy	Sat Nov 03 01:40:28 2001 +0100
     2.2 +++ b/src/HOLCF/Cfun1.thy	Sat Nov 03 01:41:26 2001 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  (*  Title:      HOLCF/Cfun1.thy
     2.5      ID:         $Id$
     2.6      Author:     Franz Regensburger
     2.7 -    Copyright   1993 Technische Universitaet Muenchen
     2.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.9  
    2.10  Definition of the type ->  of continuous functions.
    2.11  
     3.1 --- a/src/HOLCF/Cfun2.ML	Sat Nov 03 01:40:28 2001 +0100
     3.2 +++ b/src/HOLCF/Cfun2.ML	Sat Nov 03 01:41:26 2001 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  (*  Title:      HOLCF/Cfun2
     3.5      ID:         $Id$
     3.6      Author:     Franz Regensburger
     3.7 -    Copyright   1993 Technische Universitaet Muenchen
     3.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.9  
    3.10  Class Instance ->::(cpo,cpo)po
    3.11  *)
     4.1 --- a/src/HOLCF/Cfun2.thy	Sat Nov 03 01:40:28 2001 +0100
     4.2 +++ b/src/HOLCF/Cfun2.thy	Sat Nov 03 01:41:26 2001 +0100
     4.3 @@ -1,7 +1,7 @@
     4.4  (*  Title:      HOLCF/Cfun2.thy
     4.5      ID:         $Id$
     4.6      Author:     Franz Regensburger
     4.7 -    Copyright   1993 Technische Universitaet Muenchen
     4.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4.9  
    4.10  Class Instance ->::(cpo,cpo)po
    4.11  
     5.1 --- a/src/HOLCF/Cfun3.ML	Sat Nov 03 01:40:28 2001 +0100
     5.2 +++ b/src/HOLCF/Cfun3.ML	Sat Nov 03 01:41:26 2001 +0100
     5.3 @@ -1,7 +1,7 @@
     5.4  (*  Title:      HOLCF/Cfun3
     5.5      ID:         $Id$
     5.6      Author:     Franz Regensburger
     5.7 -    Copyright   1993 Technische Universitaet Muenchen
     5.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5.9  
    5.10  Class instance of  -> for class pcpo
    5.11  *)
     6.1 --- a/src/HOLCF/Cfun3.thy	Sat Nov 03 01:40:28 2001 +0100
     6.2 +++ b/src/HOLCF/Cfun3.thy	Sat Nov 03 01:41:26 2001 +0100
     6.3 @@ -1,7 +1,7 @@
     6.4  (*  Title:      HOLCF/Cfun3.thy
     6.5      ID:         $Id$
     6.6      Author:     Franz Regensburger
     6.7 -    Copyright   1993 Technische Universitaet Muenchen
     6.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     6.9  
    6.10  Class instance of  -> for class pcpo
    6.11  
     7.1 --- a/src/HOLCF/Cont.ML	Sat Nov 03 01:40:28 2001 +0100
     7.2 +++ b/src/HOLCF/Cont.ML	Sat Nov 03 01:41:26 2001 +0100
     7.3 @@ -1,7 +1,7 @@
     7.4  (*  Title:      HOLCF/Cont.ML
     7.5      ID:         $Id$
     7.6      Author:     Franz Regensburger
     7.7 -    Copyright   1993 Technische Universitaet Muenchen
     7.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     7.9  
    7.10  Results about continuity and monotonicity
    7.11  *)
     8.1 --- a/src/HOLCF/Cont.thy	Sat Nov 03 01:40:28 2001 +0100
     8.2 +++ b/src/HOLCF/Cont.thy	Sat Nov 03 01:41:26 2001 +0100
     8.3 @@ -1,7 +1,7 @@
     8.4  (*  Title:      HOLCF/cont.thy
     8.5      ID:         $Id$
     8.6      Author:     Franz Regensburger
     8.7 -    Copyright   1993 Technische Universitaet Muenchen
     8.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     8.9  
    8.10      Results about continuity and monotonicity
    8.11  *)
     9.1 --- a/src/HOLCF/Cprod1.ML	Sat Nov 03 01:40:28 2001 +0100
     9.2 +++ b/src/HOLCF/Cprod1.ML	Sat Nov 03 01:41:26 2001 +0100
     9.3 @@ -1,7 +1,7 @@
     9.4  (*  Title:      HOLCF/Cprod1.ML
     9.5      ID:         $Id$
     9.6      Author:     Franz Regensburger
     9.7 -    Copyright   1993  Technische Universitaet Muenchen
     9.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     9.9  
    9.10  Partial ordering for cartesian product of HOL theory Product_Type.thy
    9.11  *)
    10.1 --- a/src/HOLCF/Cprod1.thy	Sat Nov 03 01:40:28 2001 +0100
    10.2 +++ b/src/HOLCF/Cprod1.thy	Sat Nov 03 01:41:26 2001 +0100
    10.3 @@ -1,11 +1,9 @@
    10.4  (*  Title:      HOLCF/Cprod1.thy
    10.5      ID:         $Id$
    10.6      Author:     Franz Regensburger
    10.7 -    Copyright   1993  Technische Universitaet Muenchen
    10.8 -
    10.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   10.10  
   10.11  Partial ordering for cartesian product of HOL theory prod.thy
   10.12 -
   10.13  *)
   10.14  
   10.15  Cprod1 = Cfun3 +
    11.1 --- a/src/HOLCF/Cprod2.ML	Sat Nov 03 01:40:28 2001 +0100
    11.2 +++ b/src/HOLCF/Cprod2.ML	Sat Nov 03 01:41:26 2001 +0100
    11.3 @@ -1,7 +1,7 @@
    11.4  (*  Title:      HOLCF/Cprod2
    11.5      ID:         $Id$
    11.6      Author:     Franz Regensburger
    11.7 -    Copyright   1993 Technische Universitaet Muenchen
    11.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    11.9  
   11.10  Class Instance *::(pcpo,pcpo)po
   11.11  *)
    12.1 --- a/src/HOLCF/Cprod2.thy	Sat Nov 03 01:40:28 2001 +0100
    12.2 +++ b/src/HOLCF/Cprod2.thy	Sat Nov 03 01:41:26 2001 +0100
    12.3 @@ -1,7 +1,7 @@
    12.4  (*  Title:      HOLCF/Cprod2.thy
    12.5      ID:         $Id$
    12.6      Author:     Franz Regensburger
    12.7 -    Copyright   1993 Technische Universitaet Muenchen
    12.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    12.9  
   12.10  Class Instance *::(pcpo,pcpo)po
   12.11  
    13.1 --- a/src/HOLCF/Cprod3.ML	Sat Nov 03 01:40:28 2001 +0100
    13.2 +++ b/src/HOLCF/Cprod3.ML	Sat Nov 03 01:41:26 2001 +0100
    13.3 @@ -1,7 +1,7 @@
    13.4  (*  Title:      HOLCF/Cprod3
    13.5      ID:         $Id$
    13.6      Author:     Franz Regensburger
    13.7 -    Copyright   1993 Technische Universitaet Muenchen
    13.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    13.9  
   13.10  Class instance of * for class pcpo and cpo.
   13.11  *)
    14.1 --- a/src/HOLCF/Cprod3.thy	Sat Nov 03 01:40:28 2001 +0100
    14.2 +++ b/src/HOLCF/Cprod3.thy	Sat Nov 03 01:41:26 2001 +0100
    14.3 @@ -1,7 +1,7 @@
    14.4  (*  Title:      HOLCF/Cprod3.thy
    14.5      ID:         $Id$
    14.6      Author:     Franz Regensburger
    14.7 -    Copyright   1993 Technische Universitaet Muenchen
    14.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    14.9  
   14.10  Class instance of * for class pcpo and cpo.
   14.11  *)
    15.1 --- a/src/HOLCF/Discrete.ML	Sat Nov 03 01:40:28 2001 +0100
    15.2 +++ b/src/HOLCF/Discrete.ML	Sat Nov 03 01:41:26 2001 +0100
    15.3 @@ -1,7 +1,7 @@
    15.4  (*  Title:      HOLCF/Discrete.ML
    15.5      ID:         $Id$
    15.6      Author:     Tobias Nipkow
    15.7 -    Copyright   1997 TUM
    15.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    15.9  *)
   15.10  
   15.11  Goalw [undiscr_def] "undiscr(Discr x) = x";
    16.1 --- a/src/HOLCF/Discrete.thy	Sat Nov 03 01:40:28 2001 +0100
    16.2 +++ b/src/HOLCF/Discrete.thy	Sat Nov 03 01:41:26 2001 +0100
    16.3 @@ -1,9 +1,9 @@
    16.4  (*  Title:      HOLCF/Discrete.thy
    16.5      ID:         $Id$
    16.6      Author:     Tobias Nipkow
    16.7 -    Copyright   1997 TUM
    16.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    16.9  
   16.10 -Discrete CPOs
   16.11 +Discrete CPOs.
   16.12  *)
   16.13  
   16.14  Discrete = Discrete1 +
    17.1 --- a/src/HOLCF/Discrete0.ML	Sat Nov 03 01:40:28 2001 +0100
    17.2 +++ b/src/HOLCF/Discrete0.ML	Sat Nov 03 01:41:26 2001 +0100
    17.3 @@ -1,7 +1,7 @@
    17.4  (*  Title:      HOLCF/Discrete0.ML
    17.5      ID:         $Id$
    17.6      Author:     Tobias Nipkow
    17.7 -    Copyright   1997 TUM
    17.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    17.9  
   17.10  Proves that 'a discr is a po
   17.11  *)
    18.1 --- a/src/HOLCF/Discrete0.thy	Sat Nov 03 01:40:28 2001 +0100
    18.2 +++ b/src/HOLCF/Discrete0.thy	Sat Nov 03 01:41:26 2001 +0100
    18.3 @@ -1,9 +1,9 @@
    18.4  (*  Title:      HOLCF/Discrete0.thy
    18.5      ID:         $Id$
    18.6      Author:     Tobias Nipkow
    18.7 -    Copyright   1997 TUM
    18.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    18.9  
   18.10 -Discrete CPOs
   18.11 +Discrete CPOs.
   18.12  *)
   18.13  
   18.14  Discrete0 = Cont + Datatype +
    19.1 --- a/src/HOLCF/Discrete1.ML	Sat Nov 03 01:40:28 2001 +0100
    19.2 +++ b/src/HOLCF/Discrete1.ML	Sat Nov 03 01:41:26 2001 +0100
    19.3 @@ -1,7 +1,7 @@
    19.4  (*  Title:      HOLCF/Discrete1.ML
    19.5      ID:         $Id$
    19.6      Author:     Tobias Nipkow
    19.7 -    Copyright   1997 TUM
    19.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    19.9  
   19.10  Proves that 'a discr is a cpo
   19.11  *)
    20.1 --- a/src/HOLCF/Discrete1.thy	Sat Nov 03 01:40:28 2001 +0100
    20.2 +++ b/src/HOLCF/Discrete1.thy	Sat Nov 03 01:41:26 2001 +0100
    20.3 @@ -1,9 +1,9 @@
    20.4  (*  Title:      HOLCF/Discrete1.thy
    20.5      ID:         $Id$
    20.6      Author:     Tobias Nipkow
    20.7 -    Copyright   1997 TUM
    20.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    20.9  
   20.10 -Discrete CPOs
   20.11 +Discrete CPOs.
   20.12  *)
   20.13  
   20.14  Discrete1 = Discrete0 +
    21.1 --- a/src/HOLCF/Fix.ML	Sat Nov 03 01:40:28 2001 +0100
    21.2 +++ b/src/HOLCF/Fix.ML	Sat Nov 03 01:41:26 2001 +0100
    21.3 @@ -1,7 +1,7 @@
    21.4  (*  Title:      HOLCF/Fix.ML
    21.5      ID:         $Id$
    21.6      Author:     Franz Regensburger
    21.7 -    Copyright   1993  Technische Universitaet Muenchen
    21.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    21.9  
   21.10  fixed point operator and admissibility
   21.11  *)
    22.1 --- a/src/HOLCF/Fix.thy	Sat Nov 03 01:40:28 2001 +0100
    22.2 +++ b/src/HOLCF/Fix.thy	Sat Nov 03 01:41:26 2001 +0100
    22.3 @@ -1,11 +1,9 @@
    22.4  (*  Title:      HOLCF/Fix.thy
    22.5      ID:         $Id$
    22.6      Author:     Franz Regensburger
    22.7 -    Copyright   1993  Technische Universitaet Muenchen
    22.8 -
    22.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   22.10  
   22.11  definitions for fixed point operator and admissibility
   22.12 -
   22.13  *)
   22.14  
   22.15  Fix = Cfun3 +
    23.1 --- a/src/HOLCF/Fun1.ML	Sat Nov 03 01:40:28 2001 +0100
    23.2 +++ b/src/HOLCF/Fun1.ML	Sat Nov 03 01:41:26 2001 +0100
    23.3 @@ -1,7 +1,7 @@
    23.4  (*  Title:      HOLCF/Fun1.ML
    23.5      ID:         $Id$
    23.6      Author:     Franz Regensburger
    23.7 -    Copyright   1993  Technische Universitaet Muenchen
    23.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    23.9  
   23.10  Definition of the partial ordering for the type of all functions => (fun)
   23.11  *)
    24.1 --- a/src/HOLCF/Fun1.thy	Sat Nov 03 01:40:28 2001 +0100
    24.2 +++ b/src/HOLCF/Fun1.thy	Sat Nov 03 01:41:26 2001 +0100
    24.3 @@ -1,13 +1,11 @@
    24.4  (*  Title:      HOLCF/Fun1.thy
    24.5      ID:         $Id$
    24.6      Author:     Franz Regensburger
    24.7 -    Copyright   1993  Technische Universitaet Muenchen
    24.8 -
    24.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   24.10  
   24.11  Definition of the partial ordering for the type of all functions => (fun)
   24.12  
   24.13  REMARK: The ordering on 'a => 'b is only defined if 'b is in class po !!
   24.14 -
   24.15  *)
   24.16  
   24.17  Fun1 = Pcpo +
    25.1 --- a/src/HOLCF/Fun2.ML	Sat Nov 03 01:40:28 2001 +0100
    25.2 +++ b/src/HOLCF/Fun2.ML	Sat Nov 03 01:41:26 2001 +0100
    25.3 @@ -1,7 +1,7 @@
    25.4  (*  Title:      HOLCF/Fun2.ML
    25.5      ID:         $Id$
    25.6      Author:     Franz Regensburger
    25.7 -    Copyright   1993 Technische Universitaet Muenchen
    25.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    25.9  
   25.10  Class Instance =>::(term,po)po
   25.11  *)
    26.1 --- a/src/HOLCF/Fun2.thy	Sat Nov 03 01:40:28 2001 +0100
    26.2 +++ b/src/HOLCF/Fun2.thy	Sat Nov 03 01:41:26 2001 +0100
    26.3 @@ -1,7 +1,7 @@
    26.4  (*  Title:      HOLCF/Fun2.thy
    26.5      ID:         $Id$
    26.6      Author:     Franz Regensburger
    26.7 -    Copyright   1993 Technische Universitaet Muenchen
    26.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    26.9  
   26.10  Class Instance =>::(term,po)po
   26.11  *)
    27.1 --- a/src/HOLCF/Fun3.ML	Sat Nov 03 01:40:28 2001 +0100
    27.2 +++ b/src/HOLCF/Fun3.ML	Sat Nov 03 01:41:26 2001 +0100
    27.3 @@ -1,7 +1,7 @@
    27.4  (*  Title:      HOLCF/Fun3.ML
    27.5      ID:         $Id$
    27.6      Author:     Franz Regensburger
    27.7 -    Copyright   1993 Technische Universitaet Muenchen
    27.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    27.9  *)
   27.10  
   27.11  (* for compatibility with old HOLCF-Version *)
    28.1 --- a/src/HOLCF/Fun3.thy	Sat Nov 03 01:40:28 2001 +0100
    28.2 +++ b/src/HOLCF/Fun3.thy	Sat Nov 03 01:41:26 2001 +0100
    28.3 @@ -1,10 +1,9 @@
    28.4  (*  Title:      HOLCF/Fun3.thy
    28.5      ID:         $Id$
    28.6      Author:     Franz Regensburger
    28.7 -    Copyright   1993 Technische Universitaet Muenchen
    28.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    28.9  
   28.10  Class instance of  => (fun) for class pcpo
   28.11 -
   28.12  *)
   28.13  
   28.14  Fun3 = Fun2 +
    29.1 --- a/src/HOLCF/HOLCF.ML	Sat Nov 03 01:40:28 2001 +0100
    29.2 +++ b/src/HOLCF/HOLCF.ML	Sat Nov 03 01:41:26 2001 +0100
    29.3 @@ -1,7 +1,7 @@
    29.4  (*  Title:      HOLCF/HOLCF.ML
    29.5      ID:         $Id$
    29.6      Author:     Franz Regensburger
    29.7 -    Copyright   1993 Technische Universitaet Muenchen
    29.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    29.9  *)
   29.10  
   29.11  use"adm.ML";
    30.1 --- a/src/HOLCF/HOLCF.thy	Sat Nov 03 01:40:28 2001 +0100
    30.2 +++ b/src/HOLCF/HOLCF.thy	Sat Nov 03 01:41:26 2001 +0100
    30.3 @@ -1,11 +1,9 @@
    30.4  (*  Title:      HOLCF/HOLCF.thy
    30.5      ID:         $Id$
    30.6      Author:     Franz Regensburger
    30.7 -    Copyright   1993 Technische Universitaet Muenchen
    30.8 -
    30.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   30.10  
   30.11 -Top theory for HOLCF system
   30.12 -
   30.13 +Top theory for HOLCF system.
   30.14  *)
   30.15  
   30.16  HOLCF = Sprod3 + Ssum3 + Up3 + Lift + Discrete + One + Tr
    31.1 --- a/src/HOLCF/One.ML	Sat Nov 03 01:40:28 2001 +0100
    31.2 +++ b/src/HOLCF/One.ML	Sat Nov 03 01:41:26 2001 +0100
    31.3 @@ -1,9 +1,9 @@
    31.4  (*  Title:      HOLCF/One.ML
    31.5      ID:         $Id$
    31.6      Author:     Oscar Slotosch
    31.7 -    Copyright   1997 Technische Universitaet Muenchen
    31.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    31.9  
   31.10 -The unit domain
   31.11 +The unit domain.
   31.12  *)
   31.13  
   31.14  (* ------------------------------------------------------------------------ *)
   31.15 @@ -11,7 +11,7 @@
   31.16  (* ------------------------------------------------------------------------ *)
   31.17  
   31.18  Goalw [ONE_def] "t=UU | t = ONE";
   31.19 -by (lift.induct_tac "t" 1);
   31.20 +by (induct_tac "t" 1);
   31.21  by (Simp_tac 1);
   31.22  by (Simp_tac 1);
   31.23  qed "Exh_one";
    32.1 --- a/src/HOLCF/One.thy	Sat Nov 03 01:40:28 2001 +0100
    32.2 +++ b/src/HOLCF/One.thy	Sat Nov 03 01:41:26 2001 +0100
    32.3 @@ -1,7 +1,7 @@
    32.4  (*  Title:      HOLCF/One.thy
    32.5      ID:         $Id$
    32.6      Author:     Oscar Slotosch
    32.7 -    Copyright   1997 Technische Universitaet Muenchen
    32.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    32.9  *)
   32.10  
   32.11  One = Lift +
    33.1 --- a/src/HOLCF/Pcpo.ML	Sat Nov 03 01:40:28 2001 +0100
    33.2 +++ b/src/HOLCF/Pcpo.ML	Sat Nov 03 01:41:26 2001 +0100
    33.3 @@ -1,7 +1,7 @@
    33.4  (*  Title:      HOLCF/Pcpo.ML
    33.5      ID:         $Id$
    33.6      Author:     Franz Regensburger
    33.7 -    Copyright   1993 Technische Universitaet Muenchen
    33.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    33.9  
   33.10  introduction of the classes cpo and pcpo 
   33.11  *)
    34.1 --- a/src/HOLCF/Pcpo.thy	Sat Nov 03 01:40:28 2001 +0100
    34.2 +++ b/src/HOLCF/Pcpo.thy	Sat Nov 03 01:41:26 2001 +0100
    34.3 @@ -1,7 +1,7 @@
    34.4  (*  Title:      HOLCF/Pcpo.thy
    34.5      ID:         $Id$
    34.6      Author:     Franz Regensburger
    34.7 -    Copyright   1993 Technische Universitaet Muenchen
    34.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    34.9  
   34.10  introduction of the classes cpo and pcpo 
   34.11  *)
    35.1 --- a/src/HOLCF/Porder.ML	Sat Nov 03 01:40:28 2001 +0100
    35.2 +++ b/src/HOLCF/Porder.ML	Sat Nov 03 01:41:26 2001 +0100
    35.3 @@ -1,7 +1,7 @@
    35.4  (*  Title:      HOLCF/Porder
    35.5      ID:         $Id$
    35.6      Author:     Franz Regensburger
    35.7 -    Copyright   1993 Technische Universitaet Muenchen
    35.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    35.9  
   35.10  Conservative extension of theory Porder0 by constant definitions 
   35.11  *)
    36.1 --- a/src/HOLCF/Porder.thy	Sat Nov 03 01:40:28 2001 +0100
    36.2 +++ b/src/HOLCF/Porder.thy	Sat Nov 03 01:41:26 2001 +0100
    36.3 @@ -1,10 +1,9 @@
    36.4  (*  Title:      HOLCF/porder.thy
    36.5      ID:         $Id$
    36.6      Author:     Franz Regensburger
    36.7 -    Copyright   1993 Technische Universitaet Muenchen
    36.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    36.9  
   36.10  Conservative extension of theory Porder0 by constant definitions 
   36.11 -
   36.12  *)
   36.13  
   36.14  Porder = Porder0 +
    37.1 --- a/src/HOLCF/Porder0.ML	Sat Nov 03 01:40:28 2001 +0100
    37.2 +++ b/src/HOLCF/Porder0.ML	Sat Nov 03 01:41:26 2001 +0100
    37.3 @@ -1,9 +1,9 @@
    37.4  (*  Title:      HOLCF/Porder0.ML
    37.5      ID:         $Id$
    37.6      Author:     Oscar Slotosch
    37.7 -    Copyright   1997 Technische Universitaet Muenchen
    37.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    37.9  
   37.10 -    derive the characteristic axioms for the characteristic constants 
   37.11 +derive the characteristic axioms for the characteristic constants 
   37.12  *)
   37.13  
   37.14  AddIffs [refl_less];
    38.1 --- a/src/HOLCF/Porder0.thy	Sat Nov 03 01:40:28 2001 +0100
    38.2 +++ b/src/HOLCF/Porder0.thy	Sat Nov 03 01:41:26 2001 +0100
    38.3 @@ -1,10 +1,9 @@
    38.4  (*  Title:      HOLCF/Porder0.thy
    38.5      ID:         $Id$
    38.6      Author:     Franz Regensburger
    38.7 -    Copyright   1993 Technische Universitaet Muenchen
    38.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    38.9  
   38.10 -Definition of class porder (partial order)
   38.11 -
   38.12 +Definition of class porder (partial order).
   38.13  *)
   38.14  
   38.15  Porder0 = Main +
    39.1 --- a/src/HOLCF/Sprod0.ML	Sat Nov 03 01:40:28 2001 +0100
    39.2 +++ b/src/HOLCF/Sprod0.ML	Sat Nov 03 01:41:26 2001 +0100
    39.3 @@ -1,7 +1,7 @@
    39.4  (*  Title:      HOLCF/Sprod0
    39.5      ID:         $Id$
    39.6      Author:     Franz Regensburger
    39.7 -    Copyright   1993  Technische Universitaet Muenchen
    39.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    39.9  
   39.10  Strict product with typedef.
   39.11  *)
    40.1 --- a/src/HOLCF/Sprod0.thy	Sat Nov 03 01:40:28 2001 +0100
    40.2 +++ b/src/HOLCF/Sprod0.thy	Sat Nov 03 01:41:26 2001 +0100
    40.3 @@ -1,7 +1,7 @@
    40.4  (*  Title:      HOLCF/Sprod0.thy
    40.5      ID:         $Id$
    40.6      Author:     Franz Regensburger
    40.7 -    Copyright   1993  Technische Universitaet Muenchen
    40.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    40.9  
   40.10  Strict product with typedef.
   40.11  *)
    41.1 --- a/src/HOLCF/Sprod1.ML	Sat Nov 03 01:40:28 2001 +0100
    41.2 +++ b/src/HOLCF/Sprod1.ML	Sat Nov 03 01:41:26 2001 +0100
    41.3 @@ -1,8 +1,7 @@
    41.4  (*  Title:      HOLCF/Sprod1.ML
    41.5      ID:         $Id$
    41.6      Author:     Franz Regensburger
    41.7 -    Copyright   1993  Technische Universitaet Muenchen
    41.8 -
    41.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   41.10  *)
   41.11  
   41.12  (* ------------------------------------------------------------------------ *)
    42.1 --- a/src/HOLCF/Sprod1.thy	Sat Nov 03 01:40:28 2001 +0100
    42.2 +++ b/src/HOLCF/Sprod1.thy	Sat Nov 03 01:41:26 2001 +0100
    42.3 @@ -1,9 +1,9 @@
    42.4  (*  Title:      HOLCF/sprod1.thy
    42.5      ID:         $Id$
    42.6      Author:     Franz Regensburger
    42.7 -    Copyright   1993  Technische Universitaet Muenchen
    42.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    42.9  
   42.10 -Partial ordering for the strict product
   42.11 +Partial ordering for the strict product.
   42.12  *)
   42.13  
   42.14  Sprod1 = Sprod0 +
    43.1 --- a/src/HOLCF/Sprod2.ML	Sat Nov 03 01:40:28 2001 +0100
    43.2 +++ b/src/HOLCF/Sprod2.ML	Sat Nov 03 01:41:26 2001 +0100
    43.3 @@ -1,7 +1,7 @@
    43.4  (*  Title:      HOLCF/Sprod2.ML
    43.5      ID:         $Id$
    43.6      Author:     Franz Regensburger
    43.7 -    Copyright   1993 Technische Universitaet Muenchen
    43.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    43.9  
   43.10  Class Instance **::(pcpo,pcpo)po
   43.11  *)
    44.1 --- a/src/HOLCF/Sprod2.thy	Sat Nov 03 01:40:28 2001 +0100
    44.2 +++ b/src/HOLCF/Sprod2.thy	Sat Nov 03 01:41:26 2001 +0100
    44.3 @@ -1,7 +1,7 @@
    44.4  (*  Title:      HOLCF/Sprod2.thy
    44.5      ID:         $Id$
    44.6      Author:     Franz Regensburger
    44.7 -    Copyright   1993 Technische Universitaet Muenchen
    44.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    44.9  
   44.10  Class Instance **::(pcpo,pcpo)po
   44.11  *)
    45.1 --- a/src/HOLCF/Sprod3.ML	Sat Nov 03 01:40:28 2001 +0100
    45.2 +++ b/src/HOLCF/Sprod3.ML	Sat Nov 03 01:41:26 2001 +0100
    45.3 @@ -1,7 +1,7 @@
    45.4  (*  Title:      HOLCF/Sprod3
    45.5      ID:         $Id$
    45.6      Author:     Franz Regensburger
    45.7 -    Copyright   1993 Technische Universitaet Muenchen
    45.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    45.9  
   45.10  Class instance of  ** for class pcpo
   45.11  *)
    46.1 --- a/src/HOLCF/Sprod3.thy	Sat Nov 03 01:40:28 2001 +0100
    46.2 +++ b/src/HOLCF/Sprod3.thy	Sat Nov 03 01:41:26 2001 +0100
    46.3 @@ -1,7 +1,7 @@
    46.4  (*  Title:      HOLCF/sprod3.thy
    46.5      ID:         $Id$
    46.6      Author:     Franz Regensburger
    46.7 -    Copyright   1993 Technische Universitaet Muenchen
    46.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    46.9  
   46.10  Class instance of  ** for class pcpo
   46.11  *)
    47.1 --- a/src/HOLCF/Ssum0.ML	Sat Nov 03 01:40:28 2001 +0100
    47.2 +++ b/src/HOLCF/Ssum0.ML	Sat Nov 03 01:41:26 2001 +0100
    47.3 @@ -1,7 +1,7 @@
    47.4  (*  Title:      HOLCF/Ssum0.ML
    47.5      ID:         $Id$
    47.6      Author:     Franz Regensburger
    47.7 -    Copyright   1993  Technische Universitaet Muenchen
    47.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    47.9  
   47.10  Strict sum with typedef
   47.11  *)
    48.1 --- a/src/HOLCF/Ssum0.thy	Sat Nov 03 01:40:28 2001 +0100
    48.2 +++ b/src/HOLCF/Ssum0.thy	Sat Nov 03 01:41:26 2001 +0100
    48.3 @@ -1,7 +1,7 @@
    48.4  (*  Title:      HOLCF/Ssum0.thy
    48.5      ID:         $Id$
    48.6      Author:     Franz Regensburger
    48.7 -    Copyright   1993  Technische Universitaet Muenchen
    48.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    48.9  
   48.10  Strict sum with typedef
   48.11  *)
    49.1 --- a/src/HOLCF/Ssum1.ML	Sat Nov 03 01:40:28 2001 +0100
    49.2 +++ b/src/HOLCF/Ssum1.ML	Sat Nov 03 01:41:26 2001 +0100
    49.3 @@ -1,7 +1,7 @@
    49.4  (*  Title:      HOLCF/Ssum1.ML
    49.5      ID:         $Id$
    49.6      Author:     Franz Regensburger
    49.7 -    Copyright   1993  Technische Universitaet Muenchen
    49.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    49.9  
   49.10  Partial ordering for the strict sum ++
   49.11  *)
    50.1 --- a/src/HOLCF/Ssum1.thy	Sat Nov 03 01:40:28 2001 +0100
    50.2 +++ b/src/HOLCF/Ssum1.thy	Sat Nov 03 01:41:26 2001 +0100
    50.3 @@ -1,7 +1,7 @@
    50.4  (*  Title:      HOLCF/Ssum1.thy
    50.5      ID:         $Id$
    50.6      Author:     Franz Regensburger
    50.7 -    Copyright   1993  Technische Universitaet Muenchen
    50.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    50.9  
   50.10  Partial ordering for the strict sum ++
   50.11  *)
    51.1 --- a/src/HOLCF/Ssum2.ML	Sat Nov 03 01:40:28 2001 +0100
    51.2 +++ b/src/HOLCF/Ssum2.ML	Sat Nov 03 01:41:26 2001 +0100
    51.3 @@ -1,7 +1,7 @@
    51.4  (*  Title:      HOLCF/Ssum2.ML
    51.5      ID:         $Id$
    51.6      Author:     Franz Regensburger
    51.7 -    Copyright   1993 Technische Universitaet Muenchen
    51.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    51.9  
   51.10  Class Instance ++::(pcpo,pcpo)po
   51.11  *)
    52.1 --- a/src/HOLCF/Ssum2.thy	Sat Nov 03 01:40:28 2001 +0100
    52.2 +++ b/src/HOLCF/Ssum2.thy	Sat Nov 03 01:41:26 2001 +0100
    52.3 @@ -1,7 +1,7 @@
    52.4  (*  Title:      HOLCF/ssum2.thy
    52.5      ID:         $Id$
    52.6      Author:     Franz Regensburger
    52.7 -    Copyright   1993 Technische Universitaet Muenchen
    52.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    52.9  
   52.10  Class Instance ++::(pcpo,pcpo)po
   52.11  *)
    53.1 --- a/src/HOLCF/Ssum3.ML	Sat Nov 03 01:40:28 2001 +0100
    53.2 +++ b/src/HOLCF/Ssum3.ML	Sat Nov 03 01:41:26 2001 +0100
    53.3 @@ -1,7 +1,7 @@
    53.4  (*  Title:      HOLCF/Ssum3.ML
    53.5      ID:         $Id$
    53.6      Author:     Franz Regensburger
    53.7 -    Copyright   1993 Technische Universitaet Muenchen
    53.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    53.9  
   53.10  Class instance of  ++ for class pcpo
   53.11  *)
    54.1 --- a/src/HOLCF/Ssum3.thy	Sat Nov 03 01:40:28 2001 +0100
    54.2 +++ b/src/HOLCF/Ssum3.thy	Sat Nov 03 01:41:26 2001 +0100
    54.3 @@ -1,7 +1,7 @@
    54.4  (*  Title:      HOLCF/ssum3.thy
    54.5      ID:         $Id$
    54.6      Author:     Franz Regensburger
    54.7 -    Copyright   1993 Technische Universitaet Muenchen
    54.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    54.9  
   54.10  Class instance of  ++ for class pcpo
   54.11  *)
    55.1 --- a/src/HOLCF/Tr.ML	Sat Nov 03 01:40:28 2001 +0100
    55.2 +++ b/src/HOLCF/Tr.ML	Sat Nov 03 01:41:26 2001 +0100
    55.3 @@ -1,7 +1,7 @@
    55.4  (*  Title:      HOLCF/Tr.ML
    55.5      ID:         $Id$
    55.6      Author:     Franz Regensburger
    55.7 -    Copyright   1993 Technische Universitaet Muenchen
    55.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    55.9  
   55.10  Introduce infix if_then_else_fi and boolean connectives andalso, orelse
   55.11  *)
   55.12 @@ -11,7 +11,7 @@
   55.13  (* ------------------------------------------------------------------------ *)
   55.14  
   55.15  Goalw [FF_def,TT_def] "t=UU | t = TT | t = FF";
   55.16 -by (lift.induct_tac "t" 1);
   55.17 +by (induct_tac "t" 1);
   55.18  by (fast_tac HOL_cs 1);
   55.19  by (fast_tac (HOL_cs addss simpset()) 1);
   55.20  qed "Exh_tr";
    56.1 --- a/src/HOLCF/Tr.thy	Sat Nov 03 01:40:28 2001 +0100
    56.2 +++ b/src/HOLCF/Tr.thy	Sat Nov 03 01:41:26 2001 +0100
    56.3 @@ -1,7 +1,7 @@
    56.4  (*  Title:      HOLCF/Tr.thy
    56.5      ID:         $Id$
    56.6      Author:     Franz Regensburger
    56.7 -    Copyright   1993 Technische Universitaet Muenchen
    56.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    56.9  
   56.10  Introduce infix if_then_else_fi and boolean connectives andalso, orelse
   56.11  *)
    57.1 --- a/src/HOLCF/Up1.ML	Sat Nov 03 01:40:28 2001 +0100
    57.2 +++ b/src/HOLCF/Up1.ML	Sat Nov 03 01:41:26 2001 +0100
    57.3 @@ -1,9 +1,9 @@
    57.4  (*  Title:      HOLCF/Up1.ML
    57.5      ID:         $Id$
    57.6      Author:     Franz Regensburger
    57.7 -    Copyright   1993  Technische Universitaet Muenchen
    57.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    57.9  
   57.10 -Lifting
   57.11 +Lifting.
   57.12  *)
   57.13  
   57.14  Goal "Rep_Up (Abs_Up y) = y";
    58.1 --- a/src/HOLCF/Up1.thy	Sat Nov 03 01:40:28 2001 +0100
    58.2 +++ b/src/HOLCF/Up1.thy	Sat Nov 03 01:41:26 2001 +0100
    58.3 @@ -1,11 +1,9 @@
    58.4  (*  Title:      HOLCF/Up1.thy
    58.5      ID:         $Id$
    58.6      Author:     Franz Regensburger
    58.7 -    Copyright   1993  Technische Universitaet Muenchen
    58.8 -
    58.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   58.10  
   58.11 -Lifting
   58.12 -
   58.13 +Lifting.
   58.14  *)
   58.15  
   58.16  Up1 = Cfun3 + Sum_Type + Datatype +
    59.1 --- a/src/HOLCF/Up2.ML	Sat Nov 03 01:40:28 2001 +0100
    59.2 +++ b/src/HOLCF/Up2.ML	Sat Nov 03 01:41:26 2001 +0100
    59.3 @@ -1,7 +1,7 @@
    59.4  (*  Title:      HOLCF/Up2.ML
    59.5      ID:         $Id$
    59.6      Author:     Franz Regensburger
    59.7 -    Copyright   1993 Technische Universitaet Muenchen
    59.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    59.9  
   59.10  Class Instance u::(pcpo)po
   59.11  *)
    60.1 --- a/src/HOLCF/Up2.thy	Sat Nov 03 01:40:28 2001 +0100
    60.2 +++ b/src/HOLCF/Up2.thy	Sat Nov 03 01:41:26 2001 +0100
    60.3 @@ -1,10 +1,9 @@
    60.4  (*  Title:      HOLCF/Up2.thy
    60.5      ID:         $Id$
    60.6      Author:     Franz Regensburger
    60.7 -    Copyright   1993 Technische Universitaet Muenchen
    60.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    60.9  
   60.10  Class Instance u::(pcpo)po
   60.11 -
   60.12  *)
   60.13  
   60.14  Up2 = Up1 + 
    61.1 --- a/src/HOLCF/Up3.ML	Sat Nov 03 01:40:28 2001 +0100
    61.2 +++ b/src/HOLCF/Up3.ML	Sat Nov 03 01:41:26 2001 +0100
    61.3 @@ -1,7 +1,7 @@
    61.4  (*  Title:      HOLCF/Up3.ML
    61.5      ID:         $Id$
    61.6      Author:     Franz Regensburger
    61.7 -    Copyright   1993 Technische Universitaet Muenchen
    61.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    61.9  
   61.10  Class instance of  ('a)u for class pcpo
   61.11  *)
    62.1 --- a/src/HOLCF/Up3.thy	Sat Nov 03 01:40:28 2001 +0100
    62.2 +++ b/src/HOLCF/Up3.thy	Sat Nov 03 01:41:26 2001 +0100
    62.3 @@ -1,11 +1,9 @@
    62.4  (*  Title:      HOLCF/Up3.thy
    62.5      ID:         $Id$
    62.6      Author:     Franz Regensburger
    62.7 -    Copyright   1993 Technische Universitaet Muenchen
    62.8 -
    62.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   62.10  
   62.11  Class instance of  ('a)u for class pcpo
   62.12 -
   62.13  *)
   62.14  
   62.15  Up3 = Up2 +
    63.1 --- a/src/HOLCF/cont_consts.ML	Sat Nov 03 01:40:28 2001 +0100
    63.2 +++ b/src/HOLCF/cont_consts.ML	Sat Nov 03 01:41:26 2001 +0100
    63.3 @@ -1,6 +1,7 @@
    63.4  (*  Title:      HOLCF/cont_consts.ML
    63.5      ID:         $Id$
    63.6      Author:     Tobias Mayr and David von Oheimb
    63.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    63.8  
    63.9  Theory extender for consts section.
   63.10  *)
    64.1 --- a/src/HOLCF/domain/axioms.ML	Sat Nov 03 01:40:28 2001 +0100
    64.2 +++ b/src/HOLCF/domain/axioms.ML	Sat Nov 03 01:41:26 2001 +0100
    64.3 @@ -1,9 +1,9 @@
    64.4  (*  Title:      HOLCF/domain/axioms.ML
    64.5      ID:         $Id$
    64.6 -    Author : David von Oheimb
    64.7 -    Copyright 1995, 1996 TU Muenchen
    64.8 +    Author:     David von Oheimb
    64.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   64.10  
   64.11 -syntax generator for domain section
   64.12 +Syntax generator for domain section.
   64.13  *)
   64.14  
   64.15  structure Domain_Axioms = struct
    65.1 --- a/src/HOLCF/domain/extender.ML	Sat Nov 03 01:40:28 2001 +0100
    65.2 +++ b/src/HOLCF/domain/extender.ML	Sat Nov 03 01:41:26 2001 +0100
    65.3 @@ -1,7 +1,7 @@
    65.4  (*  Title:      HOLCF/domain/extender.ML
    65.5      ID:         $Id$
    65.6 -    Author : David von Oheimb
    65.7 -    Copyright 1995, 1996 TU Muenchen
    65.8 +    Author:     David von Oheimb
    65.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   65.10  
   65.11  Theory extender for domain section.
   65.12  *)
    66.1 --- a/src/HOLCF/domain/interface.ML	Sat Nov 03 01:40:28 2001 +0100
    66.2 +++ b/src/HOLCF/domain/interface.ML	Sat Nov 03 01:41:26 2001 +0100
    66.3 @@ -1,9 +1,9 @@
    66.4  (*  Title:      HOLCF/domain/interface.ML
    66.5      ID:         $Id$
    66.6 -    Author : David von Oheimb
    66.7 -    Copyright 1995, 1996 TU Muenchen
    66.8 +    Author:     David von Oheimb
    66.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   66.10  
   66.11 -parser for domain section
   66.12 +Parser for domain section.
   66.13  *)
   66.14  
   66.15  local 
    67.1 --- a/src/HOLCF/domain/library.ML	Sat Nov 03 01:40:28 2001 +0100
    67.2 +++ b/src/HOLCF/domain/library.ML	Sat Nov 03 01:41:26 2001 +0100
    67.3 @@ -1,9 +1,9 @@
    67.4  (*  Title:      HOLCF/domain/library.ML
    67.5      ID:         $Id$
    67.6 -    Author : David von Oheimb
    67.7 -    Copyright 1995, 1996 TU Muenchen
    67.8 +    Author:     David von Oheimb
    67.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   67.10  
   67.11 -library for domain section
   67.12 +Library for domain section.
   67.13  *)
   67.14  
   67.15  
    68.1 --- a/src/HOLCF/domain/syntax.ML	Sat Nov 03 01:40:28 2001 +0100
    68.2 +++ b/src/HOLCF/domain/syntax.ML	Sat Nov 03 01:41:26 2001 +0100
    68.3 @@ -1,9 +1,9 @@
    68.4  (*  Title:      HOLCF/domain/syntax.ML
    68.5      ID:         $Id$
    68.6 -    Author : David von Oheimb
    68.7 -    Copyright 1995, 1996 TU Muenchen
    68.8 +    Author:     David von Oheimb
    68.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   68.10  
   68.11 -syntax generator for domain section
   68.12 +Syntax generator for domain section.
   68.13  *)
   68.14  
   68.15  structure Domain_Syntax = struct 
    69.1 --- a/src/HOLCF/domain/theorems.ML	Sat Nov 03 01:40:28 2001 +0100
    69.2 +++ b/src/HOLCF/domain/theorems.ML	Sat Nov 03 01:41:26 2001 +0100
    69.3 @@ -1,9 +1,9 @@
    69.4  (*  Title:      HOLCF/domain/theorems.ML
    69.5      ID:         $Id$
    69.6 -    Author : David von Oheimb
    69.7 -    Copyright 1995, 1996 TU Muenchen
    69.8 +    Author:     David von Oheimb
    69.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   69.10  
   69.11 -proof generator for domain section
   69.12 +Proof generator for domain section.
   69.13  *)
   69.14  
   69.15  
    70.1 --- a/src/HOLCF/holcf_logic.ML	Sat Nov 03 01:40:28 2001 +0100
    70.2 +++ b/src/HOLCF/holcf_logic.ML	Sat Nov 03 01:41:26 2001 +0100
    70.3 @@ -1,6 +1,7 @@
    70.4  (*  Title:      HOLCF/holcf_logic.ML
    70.5      ID:         $Id$
    70.6      Author:     David von Oheimb
    70.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    70.8  
    70.9  Abstract syntax operations for HOLCF.
   70.10  *)
   70.11 @@ -31,11 +32,7 @@
   70.12  structure HOLCFLogic: HOLCF_LOGIC =
   70.13  struct
   70.14  
   70.15 -local
   70.16 -
   70.17 -  open HOLogic;
   70.18 -
   70.19 -in
   70.20 +open HOLogic;
   70.21  
   70.22  fun mk_btyp t (S,T) = Type (t,[S,T]);
   70.23  val mk_prodT = mk_btyp "*";
   70.24 @@ -62,5 +59,4 @@
   70.25  val oneT      = Type (intern "one",[ ]);
   70.26  end;
   70.27  
   70.28 -end; (* local *)
   70.29 -end; (* struct *)
   70.30 +end;