| Wed, 06 Aug 2008 00:58:27 +0200 |
berghofe |
Reverted last change, since it caused incompatibilities.
|
file |
diff |
annotate
|
| Mon, 04 Aug 2008 18:57:35 +0200 |
berghofe |
Quoted terms in consts_code declarations are now preprocessed as well.
|
file |
diff |
annotate
|
| Mon, 30 Jun 2008 13:41:33 +0200 |
haftmann |
simplified retrieval of theory names of consts and types
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 17:38:32 +0200 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 21:00:26 +0200 |
haftmann |
type constructors now with markup
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 18:54:59 +0200 |
wenzelm |
OldGoals.simple_read_term;
|
file |
diff |
annotate
|
| Fri, 23 May 2008 16:37:57 +0200 |
berghofe |
Replaced Pretty.str and Pretty.string_of by specific functions that
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 15:31:42 +0200 |
wenzelm |
cat_lines;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 16:30:45 +0200 |
wenzelm |
Pretty.mark;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:35 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 00:02:54 +0100 |
wenzelm |
reorganized signature of ML_Context;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
| Mon, 24 Mar 2008 23:34:24 +0100 |
wenzelm |
ML runtime compilation: pass position, tuned signature;
|
file |
diff |
annotate
|
| Thu, 10 Jan 2008 19:28:02 +0100 |
berghofe |
Test data generation and conversion to terms are now more closely
|
file |
diff |
annotate
|
| 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
|