Mon, 04 May 2020 17:35:29 +0200 Manuel Eberl New HOL simproc 'datatype_no_proper_subterm'
Tue, 12 May 2020 16:53:13 +0100 paulson merged
Tue, 12 May 2020 16:53:02 +0100 paulson Fixes for Sup{} = (0::nat)
Tue, 12 May 2020 15:11:20 +0100 paulson abbrevs for the Uniq quantifier; trying Sup_nat_def to allow zero (experimentally)
Tue, 12 May 2020 16:29:26 +0200 wenzelm clarified session imports: avoid bulky HOL-Library image;
Tue, 12 May 2020 15:52:17 +0200 wenzelm tuned -- avoid warning;
Tue, 12 May 2020 10:59:59 +0200 nipkow "app" -> "join" for RBTs
Tue, 12 May 2020 10:24:53 +0200 nipkow "app" -> "join" for uniformity with Join theory; tuned defs
Mon, 11 May 2020 19:41:31 +0200 nipkow added top-level functions and tuned
Mon, 11 May 2020 11:15:41 +0100 paulson the Uniq quantifier
Sat, 09 May 2020 17:20:04 +0000 haftmann modernized notation for bit operations
Fri, 08 May 2020 13:20:02 +0200 nipkow merged
Fri, 08 May 2020 13:19:55 +0200 nipkow avoid hidden undef cases
Fri, 08 May 2020 06:26:29 +0000 haftmann explicit mask operation for bits
Fri, 08 May 2020 06:26:28 +0000 haftmann prefer _ mod 2 over of_bool (odd _)
Fri, 08 May 2020 06:26:27 +0000 haftmann less aggressive default simp rules
Wed, 06 May 2020 15:31:24 +0200 nipkow simplified and tuned
Wed, 06 May 2020 13:52:01 +0200 nipkow tuned
Wed, 06 May 2020 10:46:19 +0200 nipkow tuned
Tue, 05 May 2020 20:32:57 +0200 nipkow tuned proofs
Tue, 05 May 2020 16:44:34 +0200 nipkow tuned var. names
Mon, 04 May 2020 23:34:46 +0200 nipkow tuned var. names
Mon, 04 May 2020 16:28:39 +0200 nipkow AVL trees with balance tags
Wed, 29 Apr 2020 15:16:17 +0100 paulson A little more tidying up
Wed, 29 Apr 2020 13:18:32 +0200 nipkow tuned
Tue, 28 Apr 2020 22:55:51 +0200 nipkow merged
Tue, 28 Apr 2020 22:55:35 +0200 nipkow tuned
Tue, 28 Apr 2020 22:09:20 +0200 wenzelm merged
Tue, 28 Apr 2020 21:47:22 +0200 wenzelm added "isabelle sessions" tool;
Tue, 28 Apr 2020 19:50:36 +0200 wenzelm tuned messages;
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 tip