| Mon, 01 Dec 2008 13:43:32 +0100 |
ballarin |
Methods intro_locales and unfold_locales apply to both old and new locales.
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:04 +0100 |
haftmann |
code_include with attach
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:03 +0100 |
haftmann |
experimental implementation of a well-sorting algorithm
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:02 +0100 |
haftmann |
code_funcgr interface includes also sort algebra
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:01 +0100 |
haftmann |
exported get_accesses (for diagnostic purpose)
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:00 +0100 |
haftmann |
more means for algebra projection
|
changeset |
files
|
| Mon, 01 Dec 2008 12:16:59 +0100 |
haftmann |
consider TeX spacing conventions for punctuation marks
|
changeset |
files
|
| Sun, 30 Nov 2008 18:10:00 +0100 |
huffman |
fix typed print translation for card UNIV
|
changeset |
files
|
| Sun, 30 Nov 2008 16:00:16 +0100 |
wenzelm |
removed obsolete CVS instructions;
|
changeset |
files
|
| Sun, 30 Nov 2008 15:03:47 +0100 |
wenzelm |
fixed spelling;
|
changeset |
files
|
| Sun, 30 Nov 2008 14:43:29 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 30 Nov 2008 14:03:46 +0100 |
wenzelm |
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
|
changeset |
files
|
| Sun, 30 Nov 2008 14:03:45 +0100 |
wenzelm |
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
|
changeset |
files
|
| Sun, 30 Nov 2008 12:58:20 +0100 |
wenzelm |
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
|
changeset |
files
|
| Sun, 30 Nov 2008 12:25:54 +0100 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sat, 29 Nov 2008 19:21:32 +0100 |
wenzelm |
remove repository-only files;
|
changeset |
files
|
| Sat, 29 Nov 2008 19:20:12 +0100 |
wenzelm |
more .hgignore entries;
|
changeset |
files
|
| Sat, 29 Nov 2008 19:01:28 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 29 Nov 2008 18:26:53 +0100 |
wenzelm |
basic setup of .hgignore;
|
changeset |
files
|
| Sat, 29 Nov 2008 18:19:59 +0100 |
wenzelm |
further notes;
|
changeset |
files
|
| Sat, 29 Nov 2008 17:09:28 +0100 |
wenzelm |
Important notes on Mercurial repository access for Isabelle.
|
changeset |
files
|
| Sat, 29 Nov 2008 13:39:45 +0100 |
nipkow |
Floats for Real.
|
changeset |
files
|
| Sat, 29 Nov 2008 13:39:23 +0100 |
nipkow |
new file float_syntax.ML
|
changeset |
files
|
| Sat, 29 Nov 2008 13:37:13 +0100 |
nipkow |
New lexical item "float".
|
changeset |
files
|
| Fri, 28 Nov 2008 17:43:06 +0100 |
ballarin |
Intro_locales_tac to simplify goals involving locale predicates.
|
changeset |
files
|
| Fri, 28 Nov 2008 12:26:14 +0100 |
ballarin |
Ahere to modern naming conventions; proper treatment of internal vs external names.
|
changeset |
files
|
| Fri, 28 Nov 2008 11:55:46 +0100 |
kleing |
added Tim's find_theorems performance patch
|
changeset |
files
|
| Fri, 28 Nov 2008 11:37:20 +0100 |
kleing |
FindTheorems performance improvements (from Timothy Bourke)
|
changeset |
files
|
| Fri, 28 Nov 2008 11:14:13 +0100 |
ballarin |
Perform higher-order pattern matching during round-up.
|
changeset |
files
|
| Thu, 27 Nov 2008 21:25:34 +0100 |
ballarin |
Proper treatment of expressions with free arguments.
|
changeset |
files
|
| Thu, 27 Nov 2008 21:25:16 +0100 |
ballarin |
Roundup bound.
|
changeset |
files
|
| Thu, 27 Nov 2008 10:30:42 +0100 |
ballarin |
Tests for sublocale command.
|
changeset |
files
|
| Thu, 27 Nov 2008 10:29:07 +0100 |
ballarin |
Sublocale command.
|
changeset |
files
|
| Thu, 27 Nov 2008 10:28:27 +0100 |
ballarin |
Command to add dependencies, fixed processing of dependencies.
|
changeset |
files
|
| Thu, 27 Nov 2008 10:26:00 +0100 |
ballarin |
Fixed strange indentation.
|
changeset |
files
|
| Tue, 25 Nov 2008 23:29:26 +0100 |
huffman |
add Algebraic and Universal to imports
|
changeset |
files
|
| Tue, 25 Nov 2008 23:29:01 +0100 |
huffman |
separate run and cases combinators
|
changeset |
files
|
| Tue, 25 Nov 2008 23:28:06 +0100 |
huffman |
renamed lemma compact_minimal to compact_bot_minimal;
|
changeset |
files
|
| Tue, 25 Nov 2008 23:26:44 +0100 |
huffman |
renamed lemma compact_minimal to compact_bot_minimal
|
changeset |
files
|
| Tue, 25 Nov 2008 18:07:33 +0100 |
ballarin |
Use standard export function.
|
changeset |
files
|
| Tue, 25 Nov 2008 18:07:01 +0100 |
ballarin |
Expression types cleaned up.
|
changeset |
files
|
| Tue, 25 Nov 2008 18:06:49 +0100 |
ballarin |
Test for term patterns added.
|
changeset |
files
|
| Tue, 25 Nov 2008 18:06:21 +0100 |
ballarin |
Expression types cleaned up, proper treatment of term patterns.
|
changeset |
files
|
| Mon, 24 Nov 2008 21:09:31 +0100 |
krauss |
check for more common errors first
|
changeset |
files
|
| Mon, 24 Nov 2008 21:00:03 +0100 |
krauss |
improved error msg; tuned
|
changeset |
files
|
| Mon, 24 Nov 2008 20:12:23 +0100 |
krauss |
removed "log" again, as IntInf.log2 already exists.
|
changeset |
files
|
| Mon, 24 Nov 2008 18:05:20 +0100 |
ballarin |
Some regression tests for theorem statements.
|
changeset |
files
|
| Mon, 24 Nov 2008 18:04:21 +0100 |
ballarin |
Enable switching to new locales during session.
|
changeset |
files
|
| Mon, 24 Nov 2008 18:03:48 +0100 |
ballarin |
Read/cert_statement for theorem statements.
|
changeset |
files
|
| Mon, 24 Nov 2008 18:02:52 +0100 |
ballarin |
Generalised activation code.
|
changeset |
files
|
| Mon, 24 Nov 2008 14:23:04 +0100 |
ballarin |
More ramifications of removal of 'includes' element.
|
changeset |
files
|
| Sun, 23 Nov 2008 18:37:56 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 23 Nov 2008 17:27:15 +0100 |
wenzelm |
eliminated finish_proof, keep pre/post normalization of results separate;
|
changeset |
files
|
| Sun, 23 Nov 2008 17:25:56 +0100 |
wenzelm |
future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
|
changeset |
files
|
| Fri, 21 Nov 2008 18:02:19 +0100 |
ballarin |
Regression tests for new locale implementation.
|
changeset |
files
|
| Fri, 21 Nov 2008 18:01:39 +0100 |
ballarin |
add_locale functional.
|
changeset |
files
|
| Fri, 21 Nov 2008 15:54:53 +0100 |
paulson |
Added a line that was missing from the definition
|
changeset |
files
|
| Fri, 21 Nov 2008 14:21:42 +0100 |
krauss |
added binary logarithm
|
changeset |
files
|
| Fri, 21 Nov 2008 13:17:43 +0100 |
paulson |
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.
|
changeset |
files
|
| Fri, 21 Nov 2008 07:34:36 +0100 |
haftmann |
Name.binding
|
changeset |
files
|