Wed, 03 Mar 2010 07:36:31 -0800 | huffman | uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate | changeset | files |
Wed, 03 Mar 2010 06:48:00 -0800 | huffman | add function axiomatize_lub_take | changeset | files |