ballarin [Mon, 24 Nov 2008 14:23:04 +0100] rev 28877
More ramifications of removal of 'includes' element.
wenzelm [Sun, 23 Nov 2008 18:37:56 +0100] rev 28876
tuned;
wenzelm [Sun, 23 Nov 2008 17:27:15 +0100] rev 28875
eliminated finish_proof, keep pre/post normalization of results separate;
wenzelm [Sun, 23 Nov 2008 17:25:56 +0100] rev 28874
future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
ballarin [Fri, 21 Nov 2008 18:02:19 +0100] rev 28873
Regression tests for new locale implementation.
ballarin [Fri, 21 Nov 2008 18:01:39 +0100] rev 28872
add_locale functional.
paulson [Fri, 21 Nov 2008 15:54:53 +0100] rev 28871
Added a line that was missing from the definition
krauss [Fri, 21 Nov 2008 14:21:42 +0100] rev 28870
added binary logarithm
paulson [Fri, 21 Nov 2008 13:17:43 +0100] rev 28869
Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.
haftmann [Fri, 21 Nov 2008 07:34:36 +0100] rev 28868
Name.binding