wenzelm [Sat, 29 Nov 2008 19:21:32 +0100] rev 28912
remove repository-only files;
wenzelm [Sat, 29 Nov 2008 19:20:12 +0100] rev 28911
more .hgignore entries;
wenzelm [Sat, 29 Nov 2008 19:01:28 +0100] rev 28910
tuned;
wenzelm [Sat, 29 Nov 2008 18:26:53 +0100] rev 28909
basic setup of .hgignore;
wenzelm [Sat, 29 Nov 2008 18:19:59 +0100] rev 28908
further notes;
tuned;
wenzelm [Sat, 29 Nov 2008 17:09:28 +0100] rev 28907
Important notes on Mercurial repository access for Isabelle.
nipkow [Sat, 29 Nov 2008 13:39:45 +0100] rev 28906
Floats for Real.
nipkow [Sat, 29 Nov 2008 13:39:23 +0100] rev 28905
new file float_syntax.ML
nipkow [Sat, 29 Nov 2008 13:37:13 +0100] rev 28904
New lexical item "float".
ballarin [Fri, 28 Nov 2008 17:43:06 +0100] rev 28903
Intro_locales_tac to simplify goals involving locale predicates.
ballarin [Fri, 28 Nov 2008 12:26:14 +0100] rev 28902
Ahere to modern naming conventions; proper treatment of internal vs external names.
kleing [Fri, 28 Nov 2008 11:55:46 +0100] rev 28901
added Tim's find_theorems performance patch
kleing [Fri, 28 Nov 2008 11:37:20 +0100] rev 28900
FindTheorems performance improvements (from Timothy Bourke)
* Prefilter the list of theorems based on the constants and
free variables in Pattern search terms, before calling
Pattern.matches_subterm.
* Apply filters successively rather than running each and
then finding the intersection.
* Show the time taken to run a query.
ballarin [Fri, 28 Nov 2008 11:14:13 +0100] rev 28899
Perform higher-order pattern matching during round-up.
ballarin [Thu, 27 Nov 2008 21:25:34 +0100] rev 28898
Proper treatment of expressions with free arguments.
ballarin [Thu, 27 Nov 2008 21:25:16 +0100] rev 28897
Roundup bound.
ballarin [Thu, 27 Nov 2008 10:30:42 +0100] rev 28896
Tests for sublocale command.
ballarin [Thu, 27 Nov 2008 10:29:07 +0100] rev 28895
Sublocale command.
ballarin [Thu, 27 Nov 2008 10:28:27 +0100] rev 28894
Command to add dependencies, fixed processing of dependencies.
ballarin [Thu, 27 Nov 2008 10:26:00 +0100] rev 28893
Fixed strange indentation.
huffman [Tue, 25 Nov 2008 23:29:26 +0100] rev 28892
add Algebraic and Universal to imports
huffman [Tue, 25 Nov 2008 23:29:01 +0100] rev 28891
separate run and cases combinators
huffman [Tue, 25 Nov 2008 23:28:06 +0100] rev 28890
renamed lemma compact_minimal to compact_bot_minimal;
renamed compacts to approximants
huffman [Tue, 25 Nov 2008 23:26:44 +0100] rev 28889
renamed lemma compact_minimal to compact_bot_minimal
ballarin [Tue, 25 Nov 2008 18:07:33 +0100] rev 28888
Use standard export function.
ballarin [Tue, 25 Nov 2008 18:07:01 +0100] rev 28887
Expression types cleaned up.
ballarin [Tue, 25 Nov 2008 18:06:49 +0100] rev 28886
Test for term patterns added.
ballarin [Tue, 25 Nov 2008 18:06:21 +0100] rev 28885
Expression types cleaned up, proper treatment of term patterns.
krauss [Mon, 24 Nov 2008 21:09:31 +0100] rev 28884
check for more common errors first
krauss [Mon, 24 Nov 2008 21:00:03 +0100] rev 28883
improved error msg; tuned
krauss [Mon, 24 Nov 2008 20:12:23 +0100] rev 28882
removed "log" again, as IntInf.log2 already exists.
ballarin [Mon, 24 Nov 2008 18:05:20 +0100] rev 28881
Some regression tests for theorem statements.
ballarin [Mon, 24 Nov 2008 18:04:21 +0100] rev 28880
Enable switching to new locales during session.
ballarin [Mon, 24 Nov 2008 18:03:48 +0100] rev 28879
Read/cert_statement for theorem statements.
ballarin [Mon, 24 Nov 2008 18:02:52 +0100] rev 28878
Generalised activation code.
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
nipkow [Thu, 20 Nov 2008 22:39:12 +0100] rev 28867
added optimizer
wenzelm [Thu, 20 Nov 2008 19:43:34 +0100] rev 28866
reactivated some dead theories (based on hints by Mark Hillebrand);
haftmann [Thu, 20 Nov 2008 19:06:05 +0100] rev 28865
Locale.local_note_qualified
haftmann [Thu, 20 Nov 2008 19:06:03 +0100] rev 28864
fact table now using name bindings
haftmann [Thu, 20 Nov 2008 19:06:02 +0100] rev 28863
dropped legacy naming code
haftmann [Thu, 20 Nov 2008 14:55:28 +0100] rev 28862
tuned name bindings
haftmann [Thu, 20 Nov 2008 14:55:25 +0100] rev 28861
using name bindings
haftmann [Thu, 20 Nov 2008 14:51:40 +0100] rev 28860
name spaces and name bindings
ballarin [Thu, 20 Nov 2008 10:29:35 +0100] rev 28859
Deleted debug message (PolyML).
wenzelm [Thu, 20 Nov 2008 00:03:55 +0100] rev 28858
removed traces of former 'includes' element;
wenzelm [Thu, 20 Nov 2008 00:03:53 +0100] rev 28857
updated generated files;
wenzelm [Thu, 20 Nov 2008 00:03:47 +0100] rev 28856
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
nipkow [Wed, 19 Nov 2008 18:15:31 +0100] rev 28855
*** empty log message ***
nipkow [Wed, 19 Nov 2008 17:55:18 +0100] rev 28854
fixed
nipkow [Wed, 19 Nov 2008 17:54:55 +0100] rev 28853
Added new fold operator and renamed the old oe to fold_image.