author | wenzelm |
Mon, 16 Aug 1999 22:07:12 +0200 | |
changeset 7224 | e41e64476f9b |
parent 5132 | 24f992a25adc |
permissions | -rw-r--r-- |
4832 | 1 |
(* Title: HOL/Lex/AutoProj.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1998 TUM |
|
5 |
*) |
|
6 |
||
5069 | 7 |
Goalw [start_def] "start(q,d,f) = q"; |
5132 | 8 |
by (Simp_tac 1); |
4832 | 9 |
qed "start_conv"; |
10 |
||
5069 | 11 |
Goalw [next_def] "next(q,d,f) = d"; |
5132 | 12 |
by (Simp_tac 1); |
4832 | 13 |
qed "next_conv"; |
14 |
||
5069 | 15 |
Goalw [fin_def] "fin(q,d,f) = f"; |
5132 | 16 |
by (Simp_tac 1); |
4832 | 17 |
qed "fin_conv"; |
18 |
||
19 |
Addsimps [start_conv,next_conv,fin_conv]; |