| Mon, 02 May 2011 22:03:18 +0200 |
wenzelm |
NEWS;
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
document new type system syntax
|
file |
diff |
annotate
|
| Sun, 01 May 2011 17:13:44 +0200 |
wenzelm |
localized \isabellestyle;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2011 21:06:04 +0200 |
wenzelm |
literal facts `prop` may contain dummy patterns;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 13:21:12 +0200 |
wenzelm |
predefined LaTeX macros for \<bind> and \<then>;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 15:58:05 +0200 |
wenzelm |
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 22:21:34 +0200 |
wenzelm |
refined PARALLEL_GOALS;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 13:48:45 +0200 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 13:33:46 +0200 |
wenzelm |
typed_print_translation: discontinued show_sorts argument;
|
file |
diff |
annotate
|
| Tue, 05 Apr 2011 15:15:33 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 04 Apr 2011 19:09:10 +0200 |
blanchet |
document "type_sys" option
|
file |
diff |
annotate
|
| Tue, 05 Apr 2011 14:25:18 +0200 |
wenzelm |
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2011 11:16:52 +0200 |
blanchet |
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 09:44:17 +0200 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Tue, 29 Mar 2011 14:27:44 +0200 |
hoelzl |
NEWS
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 20:44:47 +0100 |
wenzelm |
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 18:03:28 +0100 |
wenzelm |
enable inner syntax source positions by default (controlled via configuration option);
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 22:26:43 +0100 |
wenzelm |
NEWS: structure Timing provides various operations for timing;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 22:55:28 +0100 |
blanchet |
added "simp:", "intro:", and "elim:" to "try" command
|
file |
diff |
annotate
|
| Thu, 17 Mar 2011 22:07:17 +0100 |
blanchet |
reintroduced "show_skolems" option -- useful when too many Skolems are displayed
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 20:56:00 +0100 |
wenzelm |
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 19:16:19 +0100 |
wenzelm |
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP -- discontinued implicit detection;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 17:28:14 +0100 |
wenzelm |
clarified ISABELLE_CSDP setting (formerly CSDP_EXE);
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 16:01:00 +0100 |
wenzelm |
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 18:10:28 +0100 |
wenzelm |
discontinued legacy load path;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2011 11:20:48 +0100 |
blanchet |
mention new Nitpick options
|
file |
diff |
annotate
|
| Fri, 25 Feb 2011 16:59:48 +0100 |
krauss |
removed support for tail-recursion from function package (now implemented by partial_function)
|
file |
diff |
annotate
|