equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 *) |
5 *) |
6 |
6 |
7 goalw thy [start_def] "start(q,d,f) = q"; |
7 Goalw [start_def] "start(q,d,f) = q"; |
8 by(Simp_tac 1); |
8 by(Simp_tac 1); |
9 qed "start_conv"; |
9 qed "start_conv"; |
10 |
10 |
11 goalw thy [next_def] "next(q,d,f) = d"; |
11 Goalw [next_def] "next(q,d,f) = d"; |
12 by(Simp_tac 1); |
12 by(Simp_tac 1); |
13 qed "next_conv"; |
13 qed "next_conv"; |
14 |
14 |
15 goalw thy [fin_def] "fin(q,d,f) = f"; |
15 Goalw [fin_def] "fin(q,d,f) = f"; |
16 by(Simp_tac 1); |
16 by(Simp_tac 1); |
17 qed "fin_conv"; |
17 qed "fin_conv"; |
18 |
18 |
19 Addsimps [start_conv,next_conv,fin_conv]; |
19 Addsimps [start_conv,next_conv,fin_conv]; |