Wed, 25 Jul 2001 13:13:01 +0200 | paulson | partial restructuring to reduce dependence on Axiom of Choice | file | diff | annotate |
Thu, 31 May 2001 16:50:15 +0200 | oheimb | added injective_fst_snd | file | diff | annotate |
Fri, 23 Feb 2001 16:31:18 +0100 | oheimb | removed performance leak for split_conv_tac (and corresponding safe wrapper) | file | diff | annotate |
Tue, 20 Feb 2001 18:48:34 +0100 | oheimb | simplified proofs for splitI and splitD, added splitD' | file | diff | annotate |
Fri, 02 Feb 2001 22:19:02 +0100 | wenzelm | split = split_conv (for compatibility); | file | diff | annotate |
Thu, 01 Feb 2001 20:51:48 +0100 | oheimb | converted to Isar therory, adding attributes complete_split and split_format | file | diff | annotate |