src/LCF/ex/Ex2.thy
author oheimb
Fri Jun 02 20:38:28 2000 +0200 (2000-06-02)
changeset 9028 8a1ec8f05f14
parent 4905 be73ddff6c5a
child 17248 81bf91654e73
permissions -rw-r--r--
added HOL/Prolog
wenzelm@4905
     1
wenzelm@4905
     2
(***  Example 3.8  ***)
wenzelm@4905
     3
wenzelm@4905
     4
Ex2 = LCF +
wenzelm@4905
     5
wenzelm@4905
     6
consts
wenzelm@4905
     7
  P	:: "'a => tr"
wenzelm@4905
     8
  F	:: "'a => 'a"
wenzelm@4905
     9
  G	:: "'a => 'a"
wenzelm@4905
    10
  H	:: "'a => 'b => 'b"
wenzelm@4905
    11
  K	:: "('a => 'b => 'b) => ('a => 'b => 'b)"
wenzelm@4905
    12
wenzelm@4905
    13
rules
wenzelm@4905
    14
  F_strict	"F(UU) = UU"
wenzelm@4905
    15
  K		"K = (%h x y. P(x) => y | F(h(G(x),y)))"
wenzelm@4905
    16
  H		"H = FIX(K)"
wenzelm@4905
    17
wenzelm@4905
    18
end