equal
deleted
inserted
replaced
11 Reasoning with Inductively Defined Relations in the HOL Theorem Prover. |
11 Reasoning with Inductively Defined Relations in the HOL Theorem Prover. |
12 Report 265, University of Cambridge Computer Laboratory, 1992. |
12 Report 265, University of Cambridge Computer Laboratory, 1992. |
13 *) |
13 *) |
14 |
14 |
15 |
15 |
16 Comb = Datatype + |
16 Comb = Main + |
17 |
17 |
18 (** Datatype definition of combinators S and K, with infixed application **) |
18 (** Datatype definition of combinators S and K, with infixed application **) |
19 consts comb :: i |
19 consts comb :: i |
20 datatype |
20 datatype |
21 "comb" = K |
21 "comb" = K |