Fri, 07 Jan 2011 18:07:27 +0100 |
wenzelm |
do not open Codegen;
|
file |
diff |
annotate
|
Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
moving iteration of tests to the testers in quickcheck
|
file |
diff |
annotate
|
Mon, 25 Oct 2010 21:06:56 +0200 |
wenzelm |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
file |
diff |
annotate
|
Thu, 09 Sep 2010 17:23:03 +0200 |
bulwahn |
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
|
file |
diff |
annotate
|
Thu, 09 Sep 2010 16:43:57 +0200 |
bulwahn |
changing the container for the quickcheck options to a generic data
|
file |
diff |
annotate
|
Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
Wed, 11 Aug 2010 15:17:13 +0200 |
wenzelm |
use Pretty.enum convenience;
|
file |
diff |
annotate
|
Thu, 01 Jul 2010 16:54:42 +0200 |
haftmann |
qualified constants Set.member and Set.Collect
|
file |
diff |
annotate
|
Thu, 24 Jun 2010 14:19:08 +0200 |
wenzelm |
avoid equality on abstract type Pretty.T;
|
file |
diff |
annotate
|
Thu, 10 Jun 2010 12:24:02 +0200 |
haftmann |
moved inductive_codegen to place where product type is available; tuned structure name
|
file |
diff |
annotate
|
Sun, 30 May 2010 21:34:19 +0200 |
wenzelm |
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
|
file |
diff |
annotate
|
Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
Sun, 28 Mar 2010 16:59:06 +0200 |
wenzelm |
static defaults for configuration options;
|
file |
diff |
annotate
|
Sun, 28 Mar 2010 15:13:19 +0200 |
wenzelm |
use regular Attrib.config instead of low-level Config.declare/Attrib.register_config;
|
file |
diff |
annotate
|
Fri, 26 Feb 2010 09:49:00 +0100 |
bulwahn |
merged
|
file |
diff |
annotate
|
Thu, 25 Feb 2010 09:28:01 +0100 |
bulwahn |
added basic reporting of test cases to quickcheck
|
file |
diff |
annotate
|
Thu, 25 Feb 2010 22:32:09 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Sun, 07 Feb 2010 19:33:34 +0100 |
wenzelm |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
file |
diff |
annotate
|
Fri, 22 Jan 2010 16:56:51 +0100 |
haftmann |
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
|
file |
diff |
annotate
|
Fri, 27 Nov 2009 08:41:10 +0100 |
haftmann |
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
|
Thu, 19 Nov 2009 16:07:53 +0100 |
berghofe |
Added new counterexample generator SML_inductive for goals involving
|
file |
diff |
annotate
|
Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
Thu, 29 Oct 2009 23:49:55 +0100 |
wenzelm |
eliminated some old folds;
|
file |
diff |
annotate
|
Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
Tue, 27 Oct 2009 22:55:27 +0100 |
wenzelm |
Datatype.read_typ: standard argument order;
|
file |
diff |
annotate
|
Thu, 22 Oct 2009 13:48:06 +0200 |
haftmann |
map_range (and map_index) combinator
|
file |
diff |
annotate
|
Wed, 21 Oct 2009 12:12:21 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
Wed, 21 Oct 2009 12:09:37 +0200 |
haftmann |
curried inter as canonical list operation (beware of argument order)
|
file |
diff |
annotate
|
Wed, 21 Oct 2009 12:02:56 +0200 |
haftmann |
curried union as canonical list operation
|
file |
diff |
annotate
|
Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 00:52:37 +0200 |
wenzelm |
explicitly qualify Drule.standard;
|
file |
diff |
annotate
|
Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
Thu, 30 Jul 2009 15:20:57 +0200 |
haftmann |
path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
|
file |
diff |
annotate
|
Wed, 29 Jul 2009 16:48:34 +0200 |
haftmann |
cleaned up abstract tuple operations and named them consistently
|
file |
diff |
annotate
|
Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
Mon, 29 Jun 2009 12:18:57 +0200 |
haftmann |
explicit Set constructor for code generated for sets
|
file |
diff |
annotate
|
Tue, 23 Jun 2009 16:27:12 +0200 |
haftmann |
tuned interfaces of datatype module
|
file |
diff |
annotate
|
Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
Thu, 01 Jan 2009 14:23:39 +0100 |
wenzelm |
eliminated OldTerm.(add_)term_consts;
|
file |
diff |
annotate
|
Wed, 31 Dec 2008 18:53:16 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
Thu, 09 Oct 2008 08:47:27 +0200 |
haftmann |
established canonical argument order in SML code generators
|
file |
diff |
annotate
|
Sat, 09 Aug 2008 22:43:46 +0200 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
file |
diff |
annotate
|
Mon, 30 Jun 2008 13:41:33 +0200 |
haftmann |
simplified retrieval of theory names of consts and types
|
file |
diff |
annotate
|
Fri, 23 May 2008 16:41:39 +0200 |
berghofe |
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) 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
|
Sat, 17 May 2008 13:54:30 +0200 |
wenzelm |
structure Display: less pervasive operations;
|
file |
diff |
annotate
|
Wed, 07 May 2008 10:57:19 +0200 |
berghofe |
Adapted to encoding of sets as predicates
|
file |
diff |
annotate
|
Tue, 18 Sep 2007 07:36:38 +0200 |
haftmann |
separated code for inductive sequences from inductive_codegen.ML
|
file |
diff |
annotate
|
Sat, 15 Sep 2007 19:27:35 +0200 |
haftmann |
fixed title
|
file |
diff |
annotate
|
Tue, 28 Aug 2007 18:16:06 +0200 |
berghofe |
Added sequences with recursion depth limit.
|
file |
diff |
annotate
|
Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|
Thu, 02 Aug 2007 17:29:40 +0200 |
berghofe |
- Added cycle test to function mk_ind_def to avoid non-termination
|
file |
diff |
annotate
|
Wed, 11 Jul 2007 11:38:25 +0200 |
berghofe |
Improved code generator for Collect.
|
file |
diff |
annotate
|