| Fri, 12 Oct 2007 18:09:12 +0200 |
wenzelm |
eval_term: moved actual evaluation out of CRITICAL section;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 18:13:07 +0200 |
wenzelm |
Codegen.is_instance: raw match, ignore sort constraints;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 16:50:04 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2007 21:19:53 +0200 |
wenzelm |
auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 13:28:37 +0200 |
wenzelm |
Syntax.parse/check/read;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2007 13:52:50 +0200 |
wenzelm |
replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
|
file |
diff |
annotate
|
| Thu, 20 Sep 2007 16:23:12 +0200 |
berghofe |
- eval_term no longer computes result during compile time
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 18:05:37 +0200 |
wenzelm |
simplified PrintMode interfaces;
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:27:40 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 10 Sep 2007 16:09:01 +0200 |
berghofe |
Auto quickcheck now displays counterexample using Proof.goal_message
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 15:46:59 +0200 |
wenzelm |
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
|
file |
diff |
annotate
|
| Wed, 29 Aug 2007 10:20:22 +0200 |
berghofe |
Deleted unused fillin_mixfix function.
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 18:12:00 +0200 |
berghofe |
- restored old setup
|
file |
diff |
annotate
|
| Thu, 16 Aug 2007 11:45:06 +0200 |
haftmann |
fixed codegen setup
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 08:57:39 +0200 |
haftmann |
updated code generator setup
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 09:40:34 +0200 |
haftmann |
new nbe implementation
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 20:40:27 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 16:44:59 +0200 |
wenzelm |
PrintMode.with_default;
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 17:47:45 +0200 |
wenzelm |
Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 19:51:58 +0200 |
wenzelm |
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 10:22:17 +0200 |
haftmann |
consts in consts_code Isar commands are now referred to by usual term syntax
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:52 +0200 |
haftmann |
unfold attribute now also accepts HOL equations
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:36:07 +0200 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 23:29:33 +0200 |
wenzelm |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
file |
diff |
annotate
|
| Sun, 21 Jan 2007 16:43:42 +0100 |
wenzelm |
use_text: added name argument;
|
file |
diff |
annotate
|