src/HOLCF/domain/theorems.ML
changeset 2276 3eb9a113029e
parent 2267 b2326aefecbc
child 2445 51993fea433f
     1.1 --- a/src/HOLCF/domain/theorems.ML	Fri Nov 29 12:15:33 1996 +0100
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Fri Nov 29 12:16:57 1996 +0100
     1.3 @@ -1,20 +1,7 @@
     1.4 - (* theorems.ML
     1.5 -   Author : David von Oheimb
     1.6 -   Created: 06-Jun-95
     1.7 -   Updated: 08-Jun-95 first proof from cterms
     1.8 -   Updated: 26-Jun-95 proofs for exhaustion thms
     1.9 -   Updated: 27-Jun-95 proofs for discriminators, constructors and selectors
    1.10 -   Updated: 06-Jul-95 proofs for distinctness, invertibility and injectivity
    1.11 -   Updated: 17-Jul-95 proofs for induction rules
    1.12 -   Updated: 19-Jul-95 proof for co-induction rule
    1.13 -   Updated: 28-Aug-95 definedness theorems for selectors (completion)
    1.14 -   Updated: 05-Sep-95 simultaneous domain equations (main part)
    1.15 -   Updated: 11-Sep-95 simultaneous domain equations (coding finished)
    1.16 -   Updated: 13-Sep-95 simultaneous domain equations (debugging)
    1.17 -   Updated: 26-Oct-95 debugging and enhancement of proofs for take_apps, ind
    1.18 -   Updated: 16-Feb-96 bug concerning  domain Triv = triv  fixed
    1.19 -   Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
    1.20 -   Copyright 1995, 1996 TU Muenchen
    1.21 +(*  Title:      HOLCF/domain/theorems.ML
    1.22 +    ID:         $ $
    1.23 +    Author : David von Oheimb
    1.24 +    Copyright 1995, 1996 TU Muenchen
    1.25  *)
    1.26  
    1.27  structure Domain_Theorems = struct
    1.28 @@ -141,7 +128,7 @@
    1.29  in
    1.30  val cases = let 
    1.31              fun common_tac thm = rtac thm 1 THEN contr_tac 1;
    1.32 -            fun unit_tac true = common_tac liftE1
    1.33 +            fun unit_tac true = common_tac upE1
    1.34              |   unit_tac _    = all_tac;
    1.35              fun prod_tac []          = common_tac oneE
    1.36              |   prod_tac [arg]       = unit_tac (is_lazy arg)