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 = Arith + Inductive + |
16 Comb = Datatype + |
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 datatype comb = K |
19 datatype comb = K |
20 | S |
20 | S |
21 | "#" comb comb (infixl 90) |
21 | "#" comb comb (infixl 90) |