--- 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)))
--- 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)