equal
deleted
inserted
replaced
37 * Functions Min and Max on finite sets have been introduced. |
37 * Functions Min and Max on finite sets have been introduced. |
38 (theory Finite_Set) |
38 (theory Finite_Set) |
39 |
39 |
40 * attribute [symmetric] now works for relations as well; it turns |
40 * attribute [symmetric] now works for relations as well; it turns |
41 (x,y) : R^-1 into (y,x) : R, and vice versa; |
41 (x,y) : R^-1 into (y,x) : R, and vice versa; |
|
42 |
|
43 * arith(_tac) now produces a counter example if it cannot prove a theorem. |
|
44 In ProofGeneral the counter example appears in the trace buffer. |
42 |
45 |
43 * arith(_tac) does now know about div k and mod k where k is a numeral |
46 * arith(_tac) does now know about div k and mod k where k is a numeral |
44 of type nat or int. It can solve simple goals like |
47 of type nat or int. It can solve simple goals like |
45 |
48 |
46 "0 < n ==> n div 2 < (n::nat)" |
49 "0 < n ==> n div 2 < (n::nat)" |