| Sun, 03 Jun 2007 13:19:03 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Sun, 03 Jun 2007 12:58:28 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Sat, 02 Jun 2007 20:14:38 +0200 |
webertj |
extended
|
changeset |
files
|
| Sat, 02 Jun 2007 19:10:04 +0200 |
webertj |
cosmetic
|
changeset |
files
|
| Sat, 02 Jun 2007 18:35:38 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Sat, 02 Jun 2007 18:05:34 +0200 |
wenzelm |
added target/local_abbrev (from proof_context.ML);
|
changeset |
files
|
| Sat, 02 Jun 2007 18:05:33 +0200 |
wenzelm |
moved specific target/local_abbrev to theory_target.ML;
|
changeset |
files
|
| Sat, 02 Jun 2007 15:28:38 +0200 |
krauss |
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
|
changeset |
files
|
| Sat, 02 Jun 2007 15:26:32 +0200 |
krauss |
added "plural : 'a -> 'a -> 'b list -> 'a" for convenient error msg construction
|
changeset |
files
|
| Sat, 02 Jun 2007 13:52:07 +0200 |
wenzelm |
proper handling of Tools;
|
changeset |
files
|
| Sat, 02 Jun 2007 08:54:05 +0200 |
webertj |
cosmetic
|
changeset |
files
|
| Sat, 02 Jun 2007 08:50:29 +0200 |
webertj |
refute_tac made more deterministic
|
changeset |
files
|