Headers added
authorsandnerr
Mon Dec 09 19:27:07 1996 +0100 (1996-12-09)
changeset 2357dd2e5e655fd2
parent 2356 125260ef480c
child 2358 2106d61252b6
Headers added
src/HOLCF/Lift1.ML
src/HOLCF/Lift1.thy
src/HOLCF/Lift2.ML
src/HOLCF/Lift2.thy
src/HOLCF/Lift3.ML
src/HOLCF/Lift3.thy
     1.1 --- a/src/HOLCF/Lift1.ML	Mon Dec 09 19:16:20 1996 +0100
     1.2 +++ b/src/HOLCF/Lift1.ML	Mon Dec 09 19:27:07 1996 +0100
     1.3 @@ -1,4 +1,11 @@
     1.4 -(* Lift1.ML *)
     1.5 +(*  Title:      HOLCF/Lift1.ML
     1.6 +    ID:         $Id$
     1.7 +    Author:     Olaf Mueller, Robert Sandner
     1.8 +    Copyright   1996 Technische Universitaet Muenchen
     1.9 +
    1.10 +Theorems for Lift1.thy
    1.11 +*)
    1.12 +
    1.13  
    1.14  open Lift1;
    1.15  
     2.1 --- a/src/HOLCF/Lift1.thy	Mon Dec 09 19:16:20 1996 +0100
     2.2 +++ b/src/HOLCF/Lift1.thy	Mon Dec 09 19:27:07 1996 +0100
     2.3 @@ -1,3 +1,11 @@
     2.4 +(*  Title:      HOLCF/Lift1.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Olaf Mueller, Robert Sandner
     2.7 +    Copyright   1996 Technische Universitaet Muenchen
     2.8 +
     2.9 +Lifting types of class term to flat pcpo's
    2.10 +*)
    2.11 +
    2.12  Lift1 = Tr2 + 
    2.13  
    2.14  default term
     3.1 --- a/src/HOLCF/Lift2.ML	Mon Dec 09 19:16:20 1996 +0100
     3.2 +++ b/src/HOLCF/Lift2.ML	Mon Dec 09 19:27:07 1996 +0100
     3.3 @@ -1,4 +1,11 @@
     3.4 - (* Lift2.ML *)
     3.5 +(*  Title:      HOLCF/Lift2.ML
     3.6 +    ID:         $Id$
     3.7 +    Author:     Olaf Mueller, Robert Sandner
     3.8 +    Copyright   1996 Technische Universitaet Muenchen
     3.9 +
    3.10 +Theorems for Lift2.thy
    3.11 +*)
    3.12 +
    3.13  
    3.14  open Lift2;
    3.15  Addsimps [less_lift_def];
     4.1 --- a/src/HOLCF/Lift2.thy	Mon Dec 09 19:16:20 1996 +0100
     4.2 +++ b/src/HOLCF/Lift2.thy	Mon Dec 09 19:27:07 1996 +0100
     4.3 @@ -1,3 +1,11 @@
     4.4 +(*  Title:      HOLCF/Lift2.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Olaf Mueller, Robert Sandner
     4.7 +    Copyright   1996 Technische Universitaet Muenchen
     4.8 +
     4.9 +Class Instance lift::(term)po
    4.10 +*)
    4.11 +
    4.12  Lift2 = Lift1 + 
    4.13  
    4.14  default term
     5.1 --- a/src/HOLCF/Lift3.ML	Mon Dec 09 19:16:20 1996 +0100
     5.2 +++ b/src/HOLCF/Lift3.ML	Mon Dec 09 19:27:07 1996 +0100
     5.3 @@ -1,11 +1,14 @@
     5.4 -(* Lift3.ML *)
     5.5 +(*  Title:      HOLCF/Lift3.ML
     5.6 +    ID:         $Id$
     5.7 +    Author:     Olaf Mueller, Robert Sandner
     5.8 +    Copyright   1996 Technische Universitaet Muenchen
     5.9 +
    5.10 +Theorems for Lift3.thy
    5.11 +*)
    5.12 +
    5.13  
    5.14  open Lift3;
    5.15  
    5.16 -
    5.17 -
    5.18 -
    5.19 -
    5.20  (* ----------------------------------------------------------- *)
    5.21  (*                        From Undef to UU		       *)
    5.22  (* ----------------------------------------------------------- *)
     6.1 --- a/src/HOLCF/Lift3.thy	Mon Dec 09 19:16:20 1996 +0100
     6.2 +++ b/src/HOLCF/Lift3.thy	Mon Dec 09 19:27:07 1996 +0100
     6.3 @@ -1,3 +1,11 @@
     6.4 +(*  Title:      HOLCF/Lift3.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Olaf Mueller, Robert Sandner
     6.7 +    Copyright   1996 Technische Universitaet Muenchen
     6.8 +
     6.9 +Class Instance lift::(term)pcpo
    6.10 +*)
    6.11 +
    6.12  Lift3 = Lift2 + 
    6.13  
    6.14  default term