author | paulson |
Fri, 21 Nov 2003 11:15:40 +0100 | |
changeset 14265 | 95b42e69436c |
parent 12030 | 46d57d0290a2 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
9245 | 1 |
(* Title: HOLCF/Fun3.ML |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1461 | 3 |
Author: Franz Regensburger |
12030 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
243
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 |
|
2640 | 7 |
(* for compatibility with old HOLCF-Version *) |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
8 |
Goal "UU = (%x. UU)"; |
9245 | 9 |
by (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1); |
10 |
qed "inst_fun_pcpo"; |