equal
deleted
inserted
replaced
3 Author: Richard Mayr & Tobias Nipkow |
3 Author: Richard Mayr & Tobias Nipkow |
4 Copyright 1995 TUM |
4 Copyright 1995 TUM |
5 |
5 |
6 Main result: auto_chopper satisfies the is_auto_chopper specification. |
6 Main result: auto_chopper satisfies the is_auto_chopper specification. |
7 *) |
7 *) |
|
8 |
|
9 Delsimps (ex_simps @ all_simps); |
8 |
10 |
9 open AutoChopper; |
11 open AutoChopper; |
10 |
12 |
11 infix repeat_RS; |
13 infix repeat_RS; |
12 fun th1 repeat_RS th2 = ((th1 RS th2) repeat_RS th2) handle _ => th1; |
14 fun th1 repeat_RS th2 = ((th1 RS th2) repeat_RS th2) handle _ => th1; |