| Sun, 11 Nov 2007 16:50:30 +0100 |
wenzelm |
auto quickcheck: reduced messages;
|
file |
diff |
annotate
|
| Sat, 10 Nov 2007 15:58:18 +0100 |
wenzelm |
auto_quickcheck ref: set default in ProofGeneral/preferences only
|
file |
diff |
annotate
|
| Fri, 09 Nov 2007 23:24:30 +0100 |
haftmann |
explicit message for failed autoquickcheck
|
file |
diff |
annotate
|
| Thu, 08 Nov 2007 22:57:45 +0100 |
wenzelm |
oops -- avoid vacous goal message;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2007 22:36:46 +0100 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 13:12:50 +0100 |
haftmann |
autoquickcheck message
|
file |
diff |
annotate
|
| 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
|
| Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 20:38:20 +0100 |
haftmann |
cleanup
|
file |
diff |
annotate
|
| Sat, 09 Dec 2006 18:05:38 +0100 |
wenzelm |
ML_Syntax.reserved(_names);
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 22:38:30 +0100 |
wenzelm |
prefer Proof.context over Context.generic;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 00:52:03 +0100 |
wenzelm |
moved ML syntax operations to structure ML_Syntax;
|
file |
diff |
annotate
|
| Mon, 23 Oct 2006 16:49:21 +0200 |
haftmann |
switched merge_alists'' to AList.merge'' whenever appropriate
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 10:44:33 +0200 |
haftmann |
Symtab.foldl replaced by Symtab.fold
|
file |
diff |
annotate
|
| Thu, 12 Oct 2006 22:57:29 +0200 |
wenzelm |
print_evaluated_term: Toplevel.context_of;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 19:37:05 +0200 |
wenzelm |
moved Context.ml_output to Output.ml_output;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:29 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:22:24 +0200 |
haftmann |
moved base setup for evaluation oracle hier
|
file |
diff |
annotate
|
| Fri, 15 Sep 2006 22:56:13 +0200 |
wenzelm |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:37 +0200 |
wenzelm |
removed obsolete Drule.frees/vars_of etc.;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:16:54 +0200 |
wenzelm |
replaced Term.variant(list) by Name.variant(_list);
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 02:01:28 +0200 |
wenzelm |
renamed Type.(un)varifyT to Logic.(un)varifyT;
|
file |
diff |
annotate
|
| Sat, 29 Apr 2006 23:16:43 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Wed, 26 Apr 2006 22:38:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:00:56 +0200 |
wenzelm |
ignore sorts of consts declarations;
|
file |
diff |
annotate
|
| Thu, 06 Apr 2006 16:08:25 +0200 |
haftmann |
added definitional code generator module: codegen_theorems.ML
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:06 +0100 |
wenzelm |
remove (op =);
|
file |
diff |
annotate
|
| Wed, 22 Feb 2006 10:18:17 +0100 |
haftmann |
abandoned merge_alists' in favour of generic AList.merge
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:34:55 +0100 |
wenzelm |
removed distinct, renamed gen_distinct to distinct;
|
file |
diff |
annotate
|
| Wed, 08 Feb 2006 14:39:00 +0100 |
haftmann |
introduced gen_distinct in place of distinct
|
file |
diff |
annotate
|