author | wenzelm |
Thu, 14 Dec 2000 19:36:48 +0100 | |
changeset 10671 | ac6b3b671198 |
parent 8732 | aef229ca5e77 |
child 14428 | bb2b0e10d9be |
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 = 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