author | clasohm |
Thu, 29 Jun 1995 12:29:58 +0200 | |
changeset 250 | 093e273405f0 |
parent 115 | 0ec63df3ae04 |
permissions | -rw-r--r-- |
115
0ec63df3ae04
HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword
lcp
parents:
diff
changeset
|
1 |
(* Title: HOL/Fun.thy |
0ec63df3ae04
HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword
lcp
parents:
diff
changeset
|
2 |
ID: $Id$ |
0ec63df3ae04
HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword
lcp
parents:
diff
changeset
|
3 |
Author: Tobias Nipkow, Cambridge University Computer Laboratory |
0ec63df3ae04
HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword
lcp
parents:
diff
changeset
|
4 |
Copyright 1994 University of Cambridge |
0ec63df3ae04
HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword
lcp
parents:
diff
changeset
|
5 |
|
0ec63df3ae04
HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword
lcp
parents:
diff
changeset
|
6 |
Lemmas about functions. |
0ec63df3ae04
HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword
lcp
parents:
diff
changeset
|
7 |
*) |
0ec63df3ae04
HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword
lcp
parents:
diff
changeset
|
8 |
|
0ec63df3ae04
HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword
lcp
parents:
diff
changeset
|
9 |
Fun = Set |