equal
deleted
inserted
replaced
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 writeln"Synthesis examples, using a crude form of narrowing"; |
7 writeln"Synthesis examples, using a crude form of narrowing"; |
8 |
8 |
9 context Arith.thy; |
9 context (theory "Arith"); |
10 |
10 |
11 writeln"discovery of predecessor function"; |
11 writeln"discovery of predecessor function"; |
12 Goal |
12 Goal |
13 "?a : SUM pred:?A . Eq(N, pred`0, 0) \ |
13 "?a : SUM pred:?A . Eq(N, pred`0, 0) \ |
14 \ * (PROD n:N. Eq(N, pred ` succ(n), n))"; |
14 \ * (PROD n:N. Eq(N, pred ` succ(n), n))"; |