Wed, 07 Feb 2007 18:10:21 +0100 | berghofe | - Adapted to new inductive definition package | file | diff | annotate |
Mon, 05 Jun 2006 14:22:58 +0200 | krauss | Added [simp]-lemmas "in_inv_image" and "in_lex_prod" in the spirit of "in_measure". | file | diff | annotate |
Tue, 07 Mar 2006 16:03:31 +0100 | obua | Added HOL-ZF to Isabelle. | file | diff | annotate |