src/LCF/ex/Ex1.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
     1 
     2 (***  Section 10.4  ***)
     3 
     4 Ex1 = LCF +
     5 
     6 consts
     7   P	:: "'a => tr"
     8   G	:: "'a => 'a"
     9   H	:: "'a => 'a"
    10   K	:: "('a => 'a) => ('a => 'a)"
    11 
    12 rules
    13   P_strict	"P(UU) = UU"
    14   K		"K = (%h x. P(x) => x | h(h(G(x))))"
    15   H		"H = FIX(K)"
    16 
    17 end