Sun, 27 May 2007 20:04:02 +0200 huffman new proof of Cauchy product formula for series
Sat, 26 May 2007 07:26:03 +0200 nipkow What it says
Fri, 25 May 2007 21:08:53 +0200 haftmann improved error handling
Fri, 25 May 2007 21:08:52 +0200 haftmann using rudimentary class target mechanism
Fri, 25 May 2007 21:08:46 +0200 haftmann *** empty log message ***
Fri, 25 May 2007 21:08:45 +0200 haftmann fixed typo
Fri, 25 May 2007 18:25:17 +0200 huffman fix typos
Fri, 25 May 2007 18:24:11 +0200 nipkow *** empty log message ***
Fri, 25 May 2007 18:11:25 +0200 nipkow *** empty log message ***
Fri, 25 May 2007 18:10:56 +0200 nipkow *** empty log message ***
Fri, 25 May 2007 18:08:47 +0200 nipkow tuned
Fri, 25 May 2007 18:08:34 +0200 nipkow Added List_Comprehension
Fri, 25 May 2007 06:06:49 +0200 urbanc adapted to fix for fresh_fun_simp
Fri, 25 May 2007 05:18:56 +0200 urbanc took out Class.thy from the compiling process until memory problems are solved
Fri, 25 May 2007 00:36:54 +0200 huffman simplify some proofs
Thu, 24 May 2007 22:55:53 +0200 nipkow *** empty log message ***
Thu, 24 May 2007 16:52:54 +0200 obua Squared things out.
Thu, 24 May 2007 14:04:06 +0200 narboux fix a bug : the semantics of no_asm was the opposite
Thu, 24 May 2007 13:59:54 +0200 urbanc temporary fix for a bug in fresh_fun_simp
Thu, 24 May 2007 12:09:38 +0200 urbanc formalisation of my PhD (the result was correct, but the proof needed several corrections)
Thu, 24 May 2007 12:00:47 +0200 narboux add an option in fresh_fun_simp to prevent rewriting in assumptions
Thu, 24 May 2007 08:37:43 +0200 haftmann fixes tvar issue in type inference
Thu, 24 May 2007 08:37:42 +0200 haftmann tuned
Thu, 24 May 2007 08:37:41 +0200 haftmann tuned warning
Thu, 24 May 2007 08:37:39 +0200 haftmann rudimentary class target implementation
Thu, 24 May 2007 08:37:37 +0200 haftmann tuned Pure/General/name_space.ML
Thu, 24 May 2007 07:27:44 +0200 nipkow Introduced new classes monoid_add and group_add
Wed, 23 May 2007 19:23:22 +0200 huffman add lemma complete_algebra_summable_geometric
Wed, 23 May 2007 14:52:12 +0200 paulson formatting
Wed, 23 May 2007 07:00:18 +0200 huffman generalize powerseries and termdiffs lemmas using axclasses
Wed, 23 May 2007 02:50:19 +0200 huffman remove unused simproc definition
Wed, 23 May 2007 02:33:42 +0200 huffman remove redundant simproc; remove legacy ML bindings
Wed, 23 May 2007 01:46:15 +0200 huffman remove redundant simproc
Tue, 22 May 2007 21:32:04 +0200 huffman new simp rule Infinitesimal_of_hypreal_iff
Tue, 22 May 2007 19:58:54 +0200 huffman removed redundant lemmas
Tue, 22 May 2007 19:47:55 +0200 huffman generalize uniqueness of limits to class real_normed_algebra_1
Tue, 22 May 2007 17:56:06 +0200 paulson Some hacks for SPASS format
Tue, 22 May 2007 17:25:26 +0200 krauss some optimizations, cleanup
Tue, 22 May 2007 16:47:22 +0200 huffman add missing instance declarations
Tue, 22 May 2007 14:43:54 +0200 haftmann adjusted to change in Provers/Arith/combine_numerals.ML
Tue, 22 May 2007 13:55:30 +0200 haftmann adjusted to change in Provers/Arith/combine_numerals.ML
Tue, 22 May 2007 13:40:37 +0200 krauss regression tests: send failure reports to krauss@in.tum.de, too
Tue, 22 May 2007 07:29:49 +0200 huffman rename lemmas LIM_ident, isCont_ident, DERIV_ident
Tue, 22 May 2007 05:07:48 +0200 huffman remove obsolete CSeries.thy
Tue, 22 May 2007 00:38:51 +0200 huffman generalized ring_eq_cancel simprocs to class idom; removed redundant field_eq_cancel simprocs
Mon, 21 May 2007 19:43:33 +0200 huffman new field_combine_numerals simproc, which uses fractions as coefficients
Mon, 21 May 2007 19:14:12 +0200 narboux search bottom up to get the inner fresh fun
Mon, 21 May 2007 19:13:38 +0200 narboux add a bottom up search function
Mon, 21 May 2007 19:11:42 +0200 haftmann tuned
Mon, 21 May 2007 19:11:41 +0200 haftmann evaluation for integers
Mon, 21 May 2007 19:11:40 +0200 haftmann added lemma divAlg_div_mof
Mon, 21 May 2007 19:11:39 +0200 haftmann improved code for rev
Mon, 21 May 2007 19:11:38 +0200 haftmann min/max
Mon, 21 May 2007 19:05:37 +0200 huffman generalize CombineNumerals functor to allow coefficients with types other than IntInf.int
Mon, 21 May 2007 18:53:04 +0200 huffman add lemmas divide_numeral_1 and inverse_numeral_1
Mon, 21 May 2007 16:39:58 +0200 krauss fixed signature
Mon, 21 May 2007 16:22:46 +0200 krauss Method "lexicographic_order" now takes the same arguments as "auto"
Mon, 21 May 2007 16:19:56 +0200 narboux change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals
Sun, 20 May 2007 18:48:52 +0200 huffman define pi with THE instead of SOME; cleaned up
Sun, 20 May 2007 17:49:10 +0200 huffman add lemmas for sin,cos,tan of 30,45,60 degrees; cleaned up
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip