author | wenzelm |
Mon, 16 Aug 1999 22:07:12 +0200 | |
changeset 7224 | e41e64476f9b |
parent 4832 | bc11b5b06f87 |
child 8732 | aef229ca5e77 |
permissions | -rw-r--r-- |
(* 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 = Prod + 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