Fri, 04 Mar 2011 11:43:20 +0100 krauss clarified
Fri, 04 Mar 2011 11:52:54 +0100 krauss produce helpful mira summary for more errors
Fri, 04 Mar 2011 00:09:47 +0100 wenzelm eliminated prems;
Thu, 03 Mar 2011 22:06:15 +0100 wenzelm eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;
Thu, 03 Mar 2011 21:43:06 +0100 wenzelm tuned proofs -- eliminated prems;
Thu, 03 Mar 2011 18:43:15 +0100 wenzelm merged
Thu, 03 Mar 2011 14:38:31 +0100 blanchet merged
Thu, 03 Mar 2011 14:25:15 +0100 blanchet don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
Thu, 03 Mar 2011 18:42:12 +0100 wenzelm simplified Thy_Info.check_file -- discontinued load path;
Thu, 03 Mar 2011 18:10:28 +0100 wenzelm discontinued legacy load path;
Thu, 03 Mar 2011 15:56:17 +0100 wenzelm re-interpret ProofGeneralPgip.changecwd as Thy_Load.set_master_path, presuming that this is close to the intended semantics;
Thu, 03 Mar 2011 15:46:02 +0100 wenzelm modernized imports;
Thu, 03 Mar 2011 15:36:54 +0100 wenzelm observe standard header format;
Thu, 03 Mar 2011 15:19:20 +0100 wenzelm removed spurious 'unused_thms' (cf. 1a65b780bd56);
Thu, 03 Mar 2011 15:18:05 +0100 wenzelm isatest cygwin-poly-e: new memory management of polyml-svn could be more stable;
Thu, 03 Mar 2011 11:36:10 +0100 berghofe merged
Thu, 03 Mar 2011 11:15:50 +0100 berghofe merged
Thu, 03 Mar 2011 11:01:42 +0100 berghofe - Made sure that sort_defs is aware of constants introduced by add_type_def
Thu, 03 Mar 2011 11:20:48 +0100 blanchet mention new Nitpick options
Thu, 03 Mar 2011 11:20:48 +0100 blanchet simplify "need" option's syntax
Thu, 03 Mar 2011 11:20:48 +0100 blanchet renamed "preconstr" option "need"
Thu, 03 Mar 2011 10:55:41 +0100 hoelzl finally remove upper_bound_finite_set
Thu, 03 Mar 2011 15:59:44 +1100 kleing separate settings for afp test
Wed, 02 Mar 2011 15:51:22 +0100 blanchet added missing spaces in output
Wed, 02 Mar 2011 14:50:16 +0100 blanchet lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
Wed, 02 Mar 2011 13:09:57 +0100 blanchet unfold definitions in "preconstrs" option
Wed, 02 Mar 2011 13:09:57 +0100 blanchet robust handling of types occurring in "eval" and "preconstr" options but not in the goal
Wed, 02 Mar 2011 13:09:57 +0100 blanchet make "preconstr" option more robust -- shouldn't throw exceptions
Tue, 01 Mar 2011 10:40:14 +0000 paulson merged
Mon, 28 Feb 2011 15:06:55 +0000 paulson merged
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip