# HG changeset patch
# User oheimb
# Date 849266217 -3600
# Node ID 3eb9a113029e0281dc25aa19e249d8bd8d5eb4f7
# Parent  dbce3dce821a441480ebb4cc3a2140cf3faafde3
modified file headers
renamed lift to fup

diff -r dbce3dce821a -r 3eb9a113029e src/HOLCF/domain/library.ML
--- a/src/HOLCF/domain/library.ML	Fri Nov 29 12:15:33 1996 +0100
+++ b/src/HOLCF/domain/library.ML	Fri Nov 29 12:16:57 1996 +0100
@@ -1,9 +1,7 @@
-(* library.ML
-   Author : David von Oheimb
-   Created: 18-Jul-95 extracted from syntax.ML, axioms.ML, extender.ML, interface.ML
-   Updated: 30-Aug-95
-   Updated: 20-Oct-95 small improvement for atomize
-   Copyright 1995 TU Muenchen
+(*  Title:      HOLCF/domain/library.ML
+    ID:         $ $
+    Author : David von Oheimb
+    Copyright 1995, 1996 TU Muenchen
 *)
 
 (* ----- general support ---------------------------------------------------- *)
@@ -184,7 +182,7 @@
 	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
 	|   one_fun n (_,args) = let
 		val l2 = length args;
-		fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x
+		fun idxs m arg = (if is_lazy arg then fn x=> %%"fup"`%%"ID"`x
 					         else Id) (Bound(l2-m));
 		in cont_eta_contract (foldr'' 
 			(fn (a,t) => %%"ssplit"`(/\# (a,t)))
diff -r dbce3dce821a -r 3eb9a113029e src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Fri Nov 29 12:15:33 1996 +0100
+++ b/src/HOLCF/domain/theorems.ML	Fri Nov 29 12:16:57 1996 +0100
@@ -1,20 +1,7 @@
- (* theorems.ML
-   Author : David von Oheimb
-   Created: 06-Jun-95
-   Updated: 08-Jun-95 first proof from cterms
-   Updated: 26-Jun-95 proofs for exhaustion thms
-   Updated: 27-Jun-95 proofs for discriminators, constructors and selectors
-   Updated: 06-Jul-95 proofs for distinctness, invertibility and injectivity
-   Updated: 17-Jul-95 proofs for induction rules
-   Updated: 19-Jul-95 proof for co-induction rule
-   Updated: 28-Aug-95 definedness theorems for selectors (completion)
-   Updated: 05-Sep-95 simultaneous domain equations (main part)
-   Updated: 11-Sep-95 simultaneous domain equations (coding finished)
-   Updated: 13-Sep-95 simultaneous domain equations (debugging)
-   Updated: 26-Oct-95 debugging and enhancement of proofs for take_apps, ind
-   Updated: 16-Feb-96 bug concerning  domain Triv = triv  fixed
-   Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
-   Copyright 1995, 1996 TU Muenchen
+(*  Title:      HOLCF/domain/theorems.ML
+    ID:         $ $
+    Author : David von Oheimb
+    Copyright 1995, 1996 TU Muenchen
 *)
 
 structure Domain_Theorems = struct
@@ -141,7 +128,7 @@
 in
 val cases = let 
             fun common_tac thm = rtac thm 1 THEN contr_tac 1;
-            fun unit_tac true = common_tac liftE1
+            fun unit_tac true = common_tac upE1
             |   unit_tac _    = all_tac;
             fun prod_tac []          = common_tac oneE
             |   prod_tac [arg]       = unit_tac (is_lazy arg)