src/HOLCF/Fun3.ML
author paulson
Fri, 21 Nov 2003 11:15:40 +0100
changeset 14265 95b42e69436c
parent 12030 46d57d0290a2
child 14981 e73f8140af78
permissions -rw-r--r--
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 3842
diff changeset
     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
6bcb44e4d6e5 expanded tabs
clasohm
parents: 243
diff changeset
     3
    Author:     Franz Regensburger
12030
wenzelm
parents: 9248
diff changeset
     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
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 1461
diff changeset
     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
428385c4bc50 removed most batch-style proofs
paulson
parents: 3842
diff changeset
     9
by (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 3842
diff changeset
    10
qed "inst_fun_pcpo";