diff options
Diffstat (limited to 'theories/Wellfounded/Lexicographic_Exponentiation.v')
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 4ccc9e68d..ad157ea9d 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -8,12 +8,10 @@ (*i $Id$ i*) -(****************************************************************************) -(* Cristina Cornes *) -(* *) -(* From : Constructing Recursion Operators in Type Theory *) -(* L. Paulson JSC (1986) 2, 325-355 *) -(****************************************************************************) +(** Author: Cristina Cornes + + From : Constructing Recursion Operators in Type Theory + L. Paulson JSC (1986) 2, 325-355 *) Require Eqdep. Require PolyList. |