| changeset 5069 | 3ea049f7979d |
| parent 4832 | bc11b5b06f87 |
| child 5132 | 24f992a25adc |
--- a/src/HOL/Lex/AutoProj.ML Mon Jun 22 17:13:09 1998 +0200 +++ b/src/HOL/Lex/AutoProj.ML Mon Jun 22 17:26:46 1998 +0200 @@ -4,15 +4,15 @@ Copyright 1998 TUM *) -goalw thy [start_def] "start(q,d,f) = q"; +Goalw [start_def] "start(q,d,f) = q"; by(Simp_tac 1); qed "start_conv"; -goalw thy [next_def] "next(q,d,f) = d"; +Goalw [next_def] "next(q,d,f) = d"; by(Simp_tac 1); qed "next_conv"; -goalw thy [fin_def] "fin(q,d,f) = f"; +Goalw [fin_def] "fin(q,d,f) = f"; by(Simp_tac 1); qed "fin_conv";