src/HOL/Fun.thy
changeset 18154 0c05abaf6244
parent 17956 369e2af8ee45
child 19323 ec5cd5b1804c
     1.1 --- a/src/HOL/Fun.thy	Thu Nov 10 21:14:05 2005 +0100
     1.2 +++ b/src/HOL/Fun.thy	Fri Nov 11 00:09:37 2005 +0100
     1.3 @@ -2,9 +2,9 @@
     1.4      ID:         $Id$
     1.5      Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     1.6      Copyright   1994  University of Cambridge
     1.7 +*)
     1.8  
     1.9 -Notions about functions.
    1.10 -*)
    1.11 +header {* Notions about functions *}
    1.12  
    1.13  theory Fun
    1.14  imports Typedef