| author | paulson | 
| Mon, 17 Aug 1998 13:06:29 +0200 | |
| changeset 5324 | ec84178243ff | 
| parent 243 | c22b85994e17 | 
| permissions | -rw-r--r-- | 
| 
243
 
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
 
nipkow 
parents:  
diff
changeset
 | 
1  | 
(* Title: HOLCF/fun3.ML  | 
| 
 
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
 
nipkow 
parents:  
diff
changeset
 | 
2  | 
ID: $Id$  | 
| 
 
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
 
nipkow 
parents:  
diff
changeset
 | 
3  | 
Author: Franz Regensburger  | 
| 
 
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
 
nipkow 
parents:  
diff
changeset
 | 
4  | 
Copyright 1993 Technische Universitaet Muenchen  | 
| 
 
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
 
nipkow 
parents:  
diff
changeset
 | 
5  | 
*)  | 
| 
 
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
 
nipkow 
parents:  
diff
changeset
 | 
6  | 
|
| 
 
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
 
nipkow 
parents:  
diff
changeset
 | 
7  | 
open Fun3;  |