Removed nRS again because extract_rews now takes care of preserving names.
(* Title: HOL/Lex/AutoProj.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 1998 TUM
Is there an optimal order of arguments for `next'?
Currently we can have laws like `delta A (a#w) = delta A w o delta A a'
Otherwise we could have `acceps A == fin A o delta A (start A)'
and use foldl instead of foldl2.
*)
AutoProj = Main +
constdefs
start :: "'a * 'b * 'c => 'a"
"start A == fst A"
next :: "'a * 'b * 'c => 'b"
"next A == fst(snd(A))"
fin :: "'a * 'b * 'c => 'c"
"fin A == snd(snd(A))"
end