| Mon, 07 Jun 2010 17:52:30 +0200 |
berghofe |
Documented changes in induct, cases, and nominal_induct method.
|
file |
diff |
annotate
|
| Mon, 07 Jun 2010 11:42:32 +0200 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Mon, 07 Jun 2010 11:27:08 +0200 |
wenzelm |
more NEWS;
|
file |
diff |
annotate
|
| Fri, 04 Jun 2010 16:02:46 +0200 |
krauss |
NEWS (more strict internal axioms/defs format)
|
file |
diff |
annotate
|
| Fri, 04 Jun 2010 11:30:46 +0200 |
wenzelm |
spelling;
|
file |
diff |
annotate
|
| Thu, 03 Jun 2010 22:17:36 +0200 |
wenzelm |
diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
|
file |
diff |
annotate
|
| Thu, 03 Jun 2010 16:39:50 +0200 |
krauss |
clarified
|
file |
diff |
annotate
|
| Thu, 03 Jun 2010 16:39:05 +0200 |
krauss |
mention unconstrain in NEWS
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 21:53:03 +0200 |
wenzelm |
improved parallelism of proof term normalization;
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 17:52:19 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 17:52:00 +0200 |
blanchet |
update NEWS
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 15:38:47 +0200 |
blanchet |
removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 12:20:08 +0200 |
blanchet |
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
|
file |
diff |
annotate
|
| Mon, 31 May 2010 22:08:40 +0200 |
wenzelm |
notes on Isabelle/jEdit;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 21:37:42 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 27 May 2010 16:30:26 +0200 |
boehmes |
merged
|
file |
diff |
annotate
|
| Thu, 27 May 2010 14:54:13 +0200 |
boehmes |
moved SMT into the HOL image
|
file |
diff |
annotate
|
| Thu, 27 May 2010 18:10:37 +0200 |
wenzelm |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 17:41:27 +0200 |
wenzelm |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 15:28:23 +0200 |
wenzelm |
misc updates for release;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 15:15:20 +0200 |
wenzelm |
constant Rat.normalize needs to be qualified;
|
file |
diff |
annotate
|
| Sat, 22 May 2010 17:44:12 -0700 |
huffman |
NEWS: removed fixrec_simp attribute
|
file |
diff |
annotate
|
| Thu, 20 May 2010 16:35:52 +0200 |
haftmann |
turned old-style mem into an input abbreviation
|
file |
diff |
annotate
|
| Tue, 18 May 2010 19:00:55 -0700 |
huffman |
remove several redundant lemmas about floor and ceiling
|
file |
diff |
annotate
|
| Tue, 18 May 2010 00:01:51 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 17 May 2010 10:58:58 +0200 |
haftmann |
dropped old Library/Word.thy and toy example ex/Adder.thy
|
file |
diff |
annotate
|
| Tue, 18 May 2010 00:01:03 +0200 |
wenzelm |
do not open Legacy by default;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 15:11:25 +0200 |
wenzelm |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 23:40:00 +0200 |
wenzelm |
renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
|
file |
diff |
annotate
|