Isabelle is a popular generic theorem prover developed at Cambridge University and TU Munich. Existing logics like Isabelle/HOL provide a theorem proving environment ready to use for sizable applications. Isabelle may also serve as framework for rapid prototyping of deductive systems. It comes with a large library including Isabelle/HOL (classical higher-order logic), Isabelle/HOLCF (Scott's Logic for Computable Functions with HOL), Isabelle/FOL (classical and intuitionistic first-order logic), and Isabelle/ZF (Zermelo-Fraenkel set theory on top of FOL).
JFlex is a flex-like lexer generator for Java with emphasis on speed and full Unicode support. It works as a standalone tool or together with the LALR parser generators CUP and BYacc/J. JFlex has support for some not so usual features like negation in regular expressions and nested input streams. It can also read JLex specifications unchanged.