| 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
|