changeset 4832 | bc11b5b06f87 |
child 5069 | 3ea049f7979d |
4831:dae4d63a1318 | 4832:bc11b5b06f87 |
---|---|
1 (* Title: HOL/Lex/AutoProj.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1998 TUM |
|
5 *) |
|
6 |
|
7 goalw thy [start_def] "start(q,d,f) = q"; |
|
8 by(Simp_tac 1); |
|
9 qed "start_conv"; |
|
10 |
|
11 goalw thy [next_def] "next(q,d,f) = d"; |
|
12 by(Simp_tac 1); |
|
13 qed "next_conv"; |
|
14 |
|
15 goalw thy [fin_def] "fin(q,d,f) = f"; |
|
16 by(Simp_tac 1); |
|
17 qed "fin_conv"; |
|
18 |
|
19 Addsimps [start_conv,next_conv,fin_conv]; |