Fri, 26 Aug 2011 21:52:11 +0200 change default for generation of tag idempotence and tag argument equations
blanchet [Fri, 26 Aug 2011 21:52:11 +0200] rev 44540
change default for generation of tag idempotence and tag argument equations
Fri, 26 Aug 2011 15:11:33 -0700 merged
huffman [Fri, 26 Aug 2011 15:11:33 -0700] rev 44539
merged
Fri, 26 Aug 2011 15:11:26 -0700 NEWS entry for setsum_norm ~> norm_setsum
huffman [Fri, 26 Aug 2011 15:11:26 -0700] rev 44538
NEWS entry for setsum_norm ~> norm_setsum
Fri, 26 Aug 2011 15:00:00 -0700 make HOL-Probability respect set/pred distinction
huffman [Fri, 26 Aug 2011 15:00:00 -0700] rev 44537
make HOL-Probability respect set/pred distinction
Fri, 26 Aug 2011 23:14:36 +0200 merged
wenzelm [Fri, 26 Aug 2011 23:14:36 +0200] rev 44536
merged
Wed, 08 Sep 2010 16:10:49 -0700 use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)
huffman [Wed, 08 Sep 2010 16:10:49 -0700] rev 44535
use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)
Fri, 26 Aug 2011 10:38:29 -0700 merged
huffman [Fri, 26 Aug 2011 10:38:29 -0700] rev 44534
merged
Fri, 26 Aug 2011 08:56:29 -0700 generalize and simplify proof of continuous_within_sequentially
huffman [Fri, 26 Aug 2011 08:56:29 -0700] rev 44533
generalize and simplify proof of continuous_within_sequentially
Fri, 26 Aug 2011 08:12:38 -0700 add lemma sequentially_imp_eventually_within;
huffman [Fri, 26 Aug 2011 08:12:38 -0700] rev 44532
add lemma sequentially_imp_eventually_within; rename LIMSEQ_SEQ_conv2_lemma to sequentially_imp_eventually_at;
Thu, 25 Aug 2011 19:41:38 -0700 replace some continuous_on lemmas with more general versions
huffman [Thu, 25 Aug 2011 19:41:38 -0700] rev 44531
replace some continuous_on lemmas with more general versions
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip