equal
deleted
inserted
replaced
4 Copyright 1993 TU Munich |
4 Copyright 1993 TU Munich |
5 |
5 |
6 Generic simplifier, suitable for most logics. |
6 Generic simplifier, suitable for most logics. |
7 |
7 |
8 *) |
8 *) |
9 infix addsimps addeqcongs delsimps |
9 infix 4 addsimps addeqcongs delsimps |
10 setsolver setloop setmksimps setsubgoaler; |
10 setsolver setloop setmksimps setsubgoaler; |
11 |
11 |
12 signature SIMPLIFIER = |
12 signature SIMPLIFIER = |
13 sig |
13 sig |
14 type simpset |
14 type simpset |
15 val addeqcongs: simpset * thm list -> simpset |
15 val addeqcongs: simpset * thm list -> simpset |