Sat, 11 Jun 2011 07:50:28 +0200 haftmann tuned comment
Fri, 10 Jun 2011 17:52:09 +0200 blanchet name tuning
Fri, 10 Jun 2011 17:52:09 +0200 blanchet revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
Fri, 10 Jun 2011 17:52:09 +0200 blanchet don't trim proofs in debug mode
Fri, 10 Jun 2011 17:52:09 +0200 blanchet tuning
Fri, 10 Jun 2011 17:37:50 +0200 wenzelm isatest/makedist: build Isabelle/jEdit;
Fri, 10 Jun 2011 17:30:23 +0200 wenzelm makedist -j: build Isabelle/jEdit via given jedit_build component;
Fri, 10 Jun 2011 15:42:21 +0200 bulwahn adding another narrowing strategy for integers
Fri, 10 Jun 2011 15:03:29 +0200 wenzelm merged
Fri, 10 Jun 2011 12:01:15 +0200 blanchet pass --trim option to "eproof" script to speed up proof reconstruction
Fri, 10 Jun 2011 12:01:15 +0200 blanchet removed "atp" and "atps" aliases, which users should have forgotten by now if they ever used them
Fri, 10 Jun 2011 12:01:15 +0200 blanchet fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day
Fri, 10 Jun 2011 12:01:15 +0200 blanchet compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
Fri, 10 Jun 2011 14:59:30 +0200 wenzelm use existing ghc on macbroy20;
Fri, 10 Jun 2011 13:32:51 +0200 wenzelm local gensym based on Name.variant;
Fri, 10 Jun 2011 12:51:29 +0200 wenzelm uniform use of flexflex_rule;
Fri, 10 Jun 2011 11:47:52 +0200 wenzelm tuned name (cf. blast_stats);
Fri, 10 Jun 2011 11:39:23 +0200 wenzelm more official options blast_trace, blast_stats;
Thu, 09 Jun 2011 23:30:18 +0200 wenzelm merged
Thu, 09 Jun 2011 15:14:21 +0200 bulwahn merged
Thu, 09 Jun 2011 14:16:12 +0200 bulwahn resolving an issue with class instances that are pseudo functions in the OCaml code serializer
Thu, 09 Jun 2011 14:24:34 +0200 hoelzl merged
Thu, 09 Jun 2011 14:04:38 +0200 hoelzl fixed document generation for HOL
Thu, 09 Jun 2011 14:04:34 +0200 hoelzl lemma: independence is equal to mutual information = 0
Thu, 09 Jun 2011 13:55:11 +0200 hoelzl jensens inequality
Thu, 09 Jun 2011 11:50:16 +0200 hoelzl lemmas about right derivative and limits
Thu, 09 Jun 2011 11:50:16 +0200 hoelzl lemma about differences of convex functions
Thu, 09 Jun 2011 11:50:16 +0200 hoelzl lemmas relating ln x and x - 1
Tue, 31 May 2011 21:33:49 +0200 hoelzl use divide instead of inverse for the derivative of ln
Thu, 09 Jun 2011 11:57:39 +0200 bulwahn adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10
Thu, 09 Jun 2011 23:12:02 +0200 wenzelm renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
Thu, 09 Jun 2011 22:25:25 +0200 wenzelm document depth arguments of method "auto";
Thu, 09 Jun 2011 22:13:21 +0200 wenzelm clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
Thu, 09 Jun 2011 20:56:08 +0200 wenzelm clarified special incr_type_indexes;
Thu, 09 Jun 2011 20:22:22 +0200 wenzelm tuned signature: Name.invent and Name.invent_names;
Wed, 08 Jun 2011 22:16:21 +0200 wenzelm modernized structure ProofContext;
Thu, 09 Jun 2011 17:58:42 +0200 wenzelm even more robust \isaspacing;
Thu, 09 Jun 2011 17:51:49 +0200 wenzelm simplified Name.variant -- discontinued builtin fold_map;
Thu, 09 Jun 2011 17:46:25 +0200 wenzelm some attempts at robust \isaspacing so that \isa{...} can be used in section headings etc. (need to avoid `\? for some reason);
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Thu, 09 Jun 2011 15:38:49 +0200 wenzelm prefer new-style Name.invents;
Thu, 09 Jun 2011 15:37:37 +0200 wenzelm more tight name invention -- avoiding old functions;
Thu, 09 Jun 2011 11:26:25 +0200 wenzelm \frenchspacing for formal isabelle style avoids extra space in situations like ``@{text "?"}'' followed by plain text;
Thu, 09 Jun 2011 10:59:25 +0200 wenzelm tuned;
Thu, 09 Jun 2011 10:43:42 +0200 bulwahn NEWS
Thu, 09 Jun 2011 10:19:51 +0200 bulwahn correcting import theory of examples
Thu, 09 Jun 2011 09:07:13 +0200 bulwahn fixing code generation test
Thu, 09 Jun 2011 08:32:22 +0200 bulwahn removing char setup
Thu, 09 Jun 2011 08:32:21 +0200 bulwahn removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
Thu, 09 Jun 2011 08:32:19 +0200 bulwahn adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
Thu, 09 Jun 2011 08:32:18 +0200 bulwahn adding narrowing engine for existentials
Thu, 09 Jun 2011 08:32:18 +0200 bulwahn adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
Thu, 09 Jun 2011 08:32:16 +0200 bulwahn adding theory Quickcheck_Narrowing to HOL-Main image
Thu, 09 Jun 2011 08:32:15 +0200 bulwahn adapting IsaMakefile
Thu, 09 Jun 2011 08:32:14 +0200 bulwahn moving Quickcheck_Narrowing from Library to base directory
Thu, 09 Jun 2011 08:32:13 +0200 bulwahn compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
Thu, 09 Jun 2011 08:31:41 +0200 bulwahn local simp rule in List_Cset
Thu, 09 Jun 2011 00:16:28 +0200 blanchet tuning
Thu, 09 Jun 2011 00:16:28 +0200 blanchet compile
Thu, 09 Jun 2011 00:16:28 +0200 blanchet cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip