src/HOL/Lex/AutoProj.thy

--- a/src/HOL/Lex/AutoProj.thy	Wed Mar 03 22:58:23 2004 +0100
+++ b/src/HOL/Lex/AutoProj.thy	Thu Mar 04 10:04:42 2004 +0100
@@ -9,14 +9,23 @@
 and use foldl instead of foldl2.
 *)
 
-AutoProj = Main +
+theory AutoProj = Main:
 
 constdefs
  start :: "'a * 'b * 'c => 'a"
 "start A == fst A"
- next :: "'a * 'b * 'c => 'b"
+ "next" :: "'a * 'b * 'c => 'b"
 "next A == fst(snd(A))"
  fin :: "'a * 'b * 'c => 'c"
 "fin A == snd(snd(A))"
 
+lemma [simp]: "start(q,d,f) = q"
+by(simp add:start_def)
+
+lemma [simp]: "next(q,d,f) = d"
+by(simp add:next_def)
+
+lemma [simp]: "fin(q,d,f) = f"
+by(simp add:fin_def)
+
 end