modified file headers
authoroheimb
Fri Nov 29 12:16:57 1996 +0100 (1996-11-29)
changeset 22763eb9a113029e
parent 2275 dbce3dce821a
child 2277 9174de6c7143
modified file headers
renamed lift to fup
src/HOLCF/domain/library.ML
src/HOLCF/domain/theorems.ML
     1.1 --- a/src/HOLCF/domain/library.ML	Fri Nov 29 12:15:33 1996 +0100
     1.2 +++ b/src/HOLCF/domain/library.ML	Fri Nov 29 12:16:57 1996 +0100
     1.3 @@ -1,9 +1,7 @@
     1.4 -(* library.ML
     1.5 -   Author : David von Oheimb
     1.6 -   Created: 18-Jul-95 extracted from syntax.ML, axioms.ML, extender.ML, interface.ML
     1.7 -   Updated: 30-Aug-95
     1.8 -   Updated: 20-Oct-95 small improvement for atomize
     1.9 -   Copyright 1995 TU Muenchen
    1.10 +(*  Title:      HOLCF/domain/library.ML
    1.11 +    ID:         $ $
    1.12 +    Author : David von Oheimb
    1.13 +    Copyright 1995, 1996 TU Muenchen
    1.14  *)
    1.15  
    1.16  (* ----- general support ---------------------------------------------------- *)
    1.17 @@ -184,7 +182,7 @@
    1.18  	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
    1.19  	|   one_fun n (_,args) = let
    1.20  		val l2 = length args;
    1.21 -		fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x
    1.22 +		fun idxs m arg = (if is_lazy arg then fn x=> %%"fup"`%%"ID"`x
    1.23  					         else Id) (Bound(l2-m));
    1.24  		in cont_eta_contract (foldr'' 
    1.25  			(fn (a,t) => %%"ssplit"`(/\# (a,t)))
     2.1 --- a/src/HOLCF/domain/theorems.ML	Fri Nov 29 12:15:33 1996 +0100
     2.2 +++ b/src/HOLCF/domain/theorems.ML	Fri Nov 29 12:16:57 1996 +0100
     2.3 @@ -1,20 +1,7 @@
     2.4 - (* theorems.ML
     2.5 -   Author : David von Oheimb
     2.6 -   Created: 06-Jun-95
     2.7 -   Updated: 08-Jun-95 first proof from cterms
     2.8 -   Updated: 26-Jun-95 proofs for exhaustion thms
     2.9 -   Updated: 27-Jun-95 proofs for discriminators, constructors and selectors
    2.10 -   Updated: 06-Jul-95 proofs for distinctness, invertibility and injectivity
    2.11 -   Updated: 17-Jul-95 proofs for induction rules
    2.12 -   Updated: 19-Jul-95 proof for co-induction rule
    2.13 -   Updated: 28-Aug-95 definedness theorems for selectors (completion)
    2.14 -   Updated: 05-Sep-95 simultaneous domain equations (main part)
    2.15 -   Updated: 11-Sep-95 simultaneous domain equations (coding finished)
    2.16 -   Updated: 13-Sep-95 simultaneous domain equations (debugging)
    2.17 -   Updated: 26-Oct-95 debugging and enhancement of proofs for take_apps, ind
    2.18 -   Updated: 16-Feb-96 bug concerning  domain Triv = triv  fixed
    2.19 -   Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
    2.20 -   Copyright 1995, 1996 TU Muenchen
    2.21 +(*  Title:      HOLCF/domain/theorems.ML
    2.22 +    ID:         $ $
    2.23 +    Author : David von Oheimb
    2.24 +    Copyright 1995, 1996 TU Muenchen
    2.25  *)
    2.26  
    2.27  structure Domain_Theorems = struct
    2.28 @@ -141,7 +128,7 @@
    2.29  in
    2.30  val cases = let 
    2.31              fun common_tac thm = rtac thm 1 THEN contr_tac 1;
    2.32 -            fun unit_tac true = common_tac liftE1
    2.33 +            fun unit_tac true = common_tac upE1
    2.34              |   unit_tac _    = all_tac;
    2.35              fun prod_tac []          = common_tac oneE
    2.36              |   prod_tac [arg]       = unit_tac (is_lazy arg)