src/HOL/BNF/Tools/bnf_decl.ML
Wed, 27 Nov 2013 15:08:18 +0100 traytel command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it
less more (0) tip