#
438cc573 |
|
20-Aug-2019 |
wenzelm <none@none> |
clarified signature;
|
#
688e1181 |
|
03-Aug-2019 |
wenzelm <none@none> |
clarified signature;
|
#
237ef1a2 |
|
31-Jan-2019 |
wenzelm <none@none> |
prefer tail-recursive version (despite 4b99b1214034);
|
#
084c7234 |
|
14-Dec-2018 |
wenzelm <none@none> |
tuned whitespace;
|
#
2ab349d1 |
|
05-Nov-2018 |
wenzelm <none@none> |
tuned (see map_index);
|
#
5272cd12 |
|
11-May-2018 |
wenzelm <none@none> |
unused;
|
#
5036c0a7 |
|
05-May-2018 |
wenzelm <none@none> |
hexadecimal representation of byte string;
|
#
8aec7217 |
|
01-Feb-2018 |
wenzelm <none@none> |
tuned signature: more operations;
|
#
ea4853ba |
|
28-Jan-2018 |
wenzelm <none@none> |
clarified take/drop/chop prefix/suffix;
|
#
b646bfc6 |
|
28-Jan-2018 |
wenzelm <none@none> |
clarified signature;
|
#
75dc966d |
|
10-Dec-2017 |
wenzelm <none@none> |
clean log file on Windows;
|
#
d293958f |
|
26-Oct-2017 |
wenzelm <none@none> |
use Poly/ML 5.7.1 test version as default;
|
#
8bbf3333 |
|
26-May-2017 |
wenzelm <none@none> |
store errors in build db;
|
#
99b48bdf |
|
22-May-2017 |
wenzelm <none@none> |
permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;
|
#
392d2279 |
|
17-Oct-2016 |
wenzelm <none@none> |
accomodate Poly/ML repository version, which treats singleton strings as boxed;
|
#
b76ea1d3 |
|
14-Jun-2016 |
haftmann <none@none> |
non-deprecated char literals for Scala
|
#
e195e62f |
|
09-Apr-2016 |
wenzelm <none@none> |
clarified modules;
|
#
85397651 |
|
06-Apr-2016 |
wenzelm <none@none> |
clarified modules; tuned signature;
|
#
42d7f45e |
|
07-Mar-2016 |
wenzelm <none@none> |
discontinued cd, pwd;
|
#
9b94c25b |
|
06-Mar-2016 |
wenzelm <none@none> |
clarified treatment of fragments of Isabelle symbols during bootstrap;
|
#
71fe062b |
|
01-Mar-2016 |
wenzelm <none@none> |
clarified modules;
|
#
45c76ae3 |
|
29-Feb-2016 |
wenzelm <none@none> |
clarified modules;
|
#
3983ff10 |
|
19-Nov-2015 |
wenzelm <none@none> |
tuned;
|
#
9aaf58b5 |
|
18-Aug-2015 |
wenzelm <none@none> |
clarified File.standard_path vs. File.platform_path (like Isabelle/Scala operations); avoid patching of SML basis library;
|
#
1971a62a |
|
13-Aug-2015 |
wenzelm <none@none> |
tuned signature, in accordance to sortBy in Scala;
|
#
341e2b61 |
|
29-Jan-2015 |
wenzelm <none@none> |
tuned;
|
#
8ed3fa12 |
|
22-Dec-2014 |
wenzelm <none@none> |
obsolete;
|
#
fa47d33f |
|
22-Dec-2014 |
wenzelm <none@none> |
separate module Random; proper Synchronized.var;
|
#
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
#
9b96fde7 |
|
08-Oct-2014 |
wenzelm <none@none> |
eliminated some exotic combinators;
|
#
a3ab0af0 |
|
08-Oct-2014 |
wenzelm <none@none> |
tuned;
|
#
7af44a03 |
|
12-Aug-2014 |
wenzelm <none@none> |
more compact representation of special string values;
|
#
c879c9b9 |
|
10-Aug-2014 |
wenzelm <none@none> |
tuned -- avoid confusion with @{assert} for system failures (exception Fail);
|
#
616ba64e |
|
31-Jul-2014 |
wenzelm <none@none> |
more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;
|
#
2e37c423 |
|
10-Mar-2014 |
wenzelm <none@none> |
tuned messages -- in accordance to Isabelle/Scala;
|
#
42b5b84f |
|
18-Jan-2014 |
wenzelm <none@none> |
support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
|
#
df02ec48 |
|
31-May-2013 |
haftmann <none@none> |
combinator fold_range, corresponding to map_range --HG-- extra : rebase_source : 00890a01bbaaeb8673d6cbaa55d2a6f454fbd7ff
|
#
6563b0e2 |
|
14-May-2013 |
wenzelm <none@none> |
more uniform Markup.print_real;
|
#
384364c2 |
|
07-Mar-2013 |
wenzelm <none@none> |
tuned signature -- prefer terminology of Scala and Axiom;
|
#
6697c476 |
|
16-Jan-2013 |
wenzelm <none@none> |
eliminated dead code;
|
#
99d21b99 |
|
30-Dec-2012 |
wenzelm <none@none> |
tuned whitespace;
|
#
fe427b22 |
|
23-Aug-2012 |
wenzelm <none@none> |
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
|
#
8b038292 |
|
16-Jul-2012 |
wenzelm <none@none> |
replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;
|
#
074e9886 |
|
16-Apr-2012 |
wenzelm <none@none> |
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
|
#
f3f5fefc |
|
21-Mar-2012 |
wenzelm <none@none> |
prefer explicitly qualified exception List.Empty;
|
#
35d2bfa0 |
|
19-Mar-2012 |
wenzelm <none@none> |
discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);
|
#
31eb8288 |
|
19-Mar-2012 |
wenzelm <none@none> |
moved some legacy stuff;
|
#
af38b691 |
|
12-Mar-2012 |
wenzelm <none@none> |
some support for grouped list operations;
|
#
b9417313 |
|
08-Mar-2012 |
wenzelm <none@none> |
tuned;
|
#
7092e45e |
|
03-Mar-2012 |
wenzelm <none@none> |
discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);
|
#
f7737721 |
|
24-Nov-2011 |
wenzelm <none@none> |
more abstract datatype stamp, which avoids pointless allocation of mutable cells;
|
#
060482bd |
|
01-Sep-2011 |
wenzelm <none@none> |
more flexible sorting; tuned display;
|
#
e41b1b16 |
|
13-Jul-2011 |
wenzelm <none@none> |
low-level tuning;
|
#
4d559414 |
|
04-Jul-2011 |
wenzelm <none@none> |
pervasive Basic_Library in Scala; tuned;
|
#
91a4a9b9 |
|
30-Jun-2011 |
wenzelm <none@none> |
getenv_strict in ML; tuned;
|
#
c4f67d53 |
|
27-Jun-2011 |
wenzelm <none@none> |
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
|
#
390ebc4a |
|
08-Jun-2011 |
wenzelm <none@none> |
more robust exception pattern General.Subscript;
|
#
74b5e67e |
|
19-Apr-2011 |
wenzelm <none@none> |
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
|
#
2b83cab5 |
|
12-Jan-2011 |
wenzelm <none@none> |
smart_string_of_real: print integer values without fractional part;
|
#
70689405 |
|
10-Jan-2011 |
wenzelm <none@none> |
made SML/NJ happy;
|
#
9b08c6eb |
|
10-Jan-2011 |
wenzelm <none@none> |
tuned string_of_int to avoid allocation for small integers;
|
#
f1d76d3c |
|
10-Jan-2011 |
wenzelm <none@none> |
standardized split_last/last_elem towards List.last; eliminated obsolete Library.last_elem;
|
#
1e798a9c |
|
03-Dec-2010 |
krauss <none@none> |
really fixed comment (cf. 7abeb749ae99)
|
#
b6696ffe |
|
03-Dec-2010 |
bulwahn <none@none> |
fixing comment in library
|
#
6b03a31b |
|
03-Dec-2010 |
wenzelm <none@none> |
removed confusing comments (cf. 500171e7aa59);
|
#
2e3aa82a |
|
26-Nov-2010 |
haftmann <none@none> |
strict forall2
|
#
637fe2f1 |
|
26-Nov-2010 |
wenzelm <none@none> |
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
|
#
75b75b89 |
|
26-Nov-2010 |
wenzelm <none@none> |
just one version of fold_rev2;
|
#
14e6bac1 |
|
19-Nov-2010 |
wenzelm <none@none> |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
#
0c5bca9f |
|
16-Nov-2010 |
haftmann <none@none> |
added forall2 predicate lifter
|
#
15f3287d |
|
12-Nov-2010 |
wenzelm <none@none> |
tuned signatures;
|
#
1a30ae26 |
|
03-Nov-2010 |
wenzelm <none@none> |
discontinued obsolete function sys_error and exception SYS_ERROR;
|
#
e5f2a357 |
|
30-Oct-2010 |
wenzelm <none@none> |
support for real valued configuration options;
|
#
ba1e1620 |
|
01-Oct-2010 |
haftmann <none@none> |
chop_while replace drop_while and take_while
|
#
3e1f51b9 |
|
30-Sep-2010 |
haftmann <none@none> |
take_while, drop_while
|
#
0c49849b |
|
22-Sep-2010 |
wenzelm <none@none> |
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
|
#
b745eb8d |
|
20-Jul-2010 |
wenzelm <none@none> |
tuned;
|
#
4549e8d1 |
|
05-May-2010 |
haftmann <none@none> |
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 =)
|
#
89caf7ae |
|
26-Mar-2010 |
wenzelm <none@none> |
tuned white space;
|
#
ac188dc4 |
|
09-Dec-2009 |
haftmann <none@none> |
take and drop as projections of chop
|
#
e3772a5e |
|
24-Nov-2009 |
haftmann <none@none> |
curried take/drop --HG-- extra : rebase_source : 6e6b508d936640bef00f0ad0c4fb089ad5253ef0
|
#
1cc32a22 |
|
26-Oct-2009 |
haftmann <none@none> |
avoid upto if not needed
|
#
04badbb2 |
|
22-Oct-2009 |
wenzelm <none@none> |
made SML/NJ happy;
|
#
69213ca7 |
|
22-Oct-2009 |
haftmann <none@none> |
restored accidentally deleted submultiset
|
#
c0695843 |
|
22-Oct-2009 |
haftmann <none@none> |
multiset operations with canonical argument order
|
#
50da8ae7 |
|
22-Oct-2009 |
haftmann <none@none> |
map_range (and map_index) combinator
|
#
8eb709ab |
|
20-Oct-2009 |
haftmann <none@none> |
curried inter as canonical list operation (beware of argument order)
|
#
26a442f9 |
|
20-Oct-2009 |
haftmann <none@none> |
curried union as canonical list operation
|
#
d103ca85 |
|
21-Oct-2009 |
haftmann <none@none> |
removed old-style \ and \\ infixes
|
#
8de45ab6 |
|
21-Oct-2009 |
haftmann <none@none> |
dropped redundant gen_ prefix
|
#
68478f6d |
|
20-Oct-2009 |
haftmann <none@none> |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
#
60c018fa |
|
17-Oct-2009 |
wenzelm <none@none> |
tuned/moved divide_and_conquer';
|
#
b2816004 |
|
17-Oct-2009 |
wenzelm <none@none> |
indicate CRITICAL nature of various setmp combinators;
|
#
9b0c4a66 |
|
29-Sep-2009 |
wenzelm <none@none> |
Raw ML references as unsynchronized state variables.
|
#
65e15d08 |
|
09-Aug-2009 |
haftmann <none@none> |
added map_transpose
|
#
0adbf7b2 |
|
24-Jul-2009 |
wenzelm <none@none> |
eliminated redundant Library.multiply;
|
#
97037932 |
|
09-Jul-2009 |
haftmann <none@none> |
dropped find_index_eq
|
#
4b1ebad9 |
|
24-May-2009 |
haftmann <none@none> |
funpow_yield; tuned
|
#
66e1bc8c |
|
18-Mar-2009 |
wenzelm <none@none> |
Library.merge/OrdList.union: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard eq/ord notion;
|
#
f1b67dee |
|
18-Mar-2009 |
haftmann <none@none> |
made SML/NJ happy
|
#
85267125 |
|
17-Mar-2009 |
wenzelm <none@none> |
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
d647eb14 |
|
01-Mar-2009 |
wenzelm <none@none> |
use long names for old-style fold combinators;
|
#
baf63383 |
|
12-Feb-2009 |
kleing <none@none> |
New command find_consts searching for constants by type (by Timothy Bourke).
|
#
cdd7107d |
|
11-Dec-2008 |
ballarin <none@none> |
Clarified comment.
|
#
6be4dcb9 |
|
10-Nov-2008 |
haftmann <none@none> |
clarified comment
|
#
2c798618 |
|
09-Oct-2008 |
haftmann <none@none> |
removed legacy |>>>
|
#
49cb1825 |
|
25-Sep-2008 |
haftmann <none@none> |
burrow_fst
|
#
47991e88 |
|
07-Sep-2008 |
wenzelm <none@none> |
added change_result;
|
#
679698ce |
|
04-Sep-2008 |
wenzelm <none@none> |
Thread.getLocal/setLocal;
|
#
2ae075f5 |
|
27-Aug-2008 |
wenzelm <none@none> |
replaced find_substring by first_field;
|
#
5a910236 |
|
27-Aug-2008 |
wenzelm <none@none> |
added find_substring;
|
#
6269d175 |
|
13-Aug-2008 |
wenzelm <none@none> |
removed obsolete untabify (superceded by SymbolPos.tabify_content);
|
#
9a430895 |
|
27-Mar-2008 |
haftmann <none@none> |
changed wrong assignement in signature sections
|
#
fe6a99ee |
|
27-Mar-2008 |
wenzelm <none@none> |
tuned comments;
|
#
b0961a8d |
|
16-Feb-2008 |
wenzelm <none@none> |
setmp: uninterruptible;
|
#
00ca9f58 |
|
26-Jan-2008 |
wenzelm <none@none> |
added surround;
|
#
6d20754c |
|
22-Jan-2008 |
haftmann <none@none> |
added map_split
|
#
9019e46e |
|
02-Jan-2008 |
wenzelm <none@none> |
added setmp_thread_data;
|
#
c8a7e939 |
|
01-Jan-2008 |
wenzelm <none@none> |
removed separate exists/forall code;
|
#
a61e3b5f |
|
18-Dec-2007 |
wenzelm <none@none> |
serial: now based on specific version in structure Multithreading;
|
#
fa7efdef |
|
17-Dec-2007 |
berghofe <none@none> |
Added foldl1.
|
#
49a4f081 |
|
05-Dec-2007 |
wenzelm <none@none> |
tuned signature;
|
#
d338564b |
|
05-Dec-2007 |
haftmann <none@none> |
map_product and fold_product
|
#
8d8b5959 |
|
29-Oct-2007 |
wenzelm <none@none> |
added bool_ord;
|
#
6b2f3b2b |
|
16-Oct-2007 |
haftmann <none@none> |
added yield_singleton
|
#
698b4f91 |
|
16-Oct-2007 |
wenzelm <none@none> |
added perhaps_apply/loop;
|
#
c680fdc8 |
|
11-Oct-2007 |
wenzelm <none@none> |
removed obsolete flip;
|
#
eef375eb |
|
05-Oct-2007 |
wenzelm <none@none> |
added burrow_options;
|
#
76d86924 |
|
04-Oct-2007 |
haftmann <none@none> |
added nth_drop
|
#
2a4bde03 |
|
18-Sep-2007 |
wenzelm <none@none> |
simplified type int (eliminated IntInf.int, integer);
|
#
ae3b0c4f |
|
16-Sep-2007 |
wenzelm <none@none> |
added some int constraints (ML_Parse.fix_ints not active here);
|
#
7732e056 |
|
03-Aug-2007 |
wenzelm <none@none> |
named some CRITICAL sections;
|
#
4abc864a |
|
29-Jul-2007 |
wenzelm <none@none> |
added list update;
|
#
850a4dab |
|
28-Jul-2007 |
wenzelm <none@none> |
setmp: NAMED_CRITICAL;
|
#
9473e8a6 |
|
24-Jul-2007 |
wenzelm <none@none> |
moved exception capture/release to structure Exn;
|
#
8d01d98a |
|
23-Jul-2007 |
wenzelm <none@none> |
eliminated transform_failure (to avoid critical section for main transactions);
|
#
337adc5c |
|
23-Jul-2007 |
wenzelm <none@none> |
added setmp_noncritical; setmp: CRITICAL;
|
#
cd9547d7 |
|
23-Jul-2007 |
wenzelm <none@none> |
marked some CRITICAL sections (for multithreading);
|
#
9753db80 |
|
19-Jul-2007 |
wenzelm <none@none> |
added undefined: 'a -> 'b;
|
#
949e4b6c |
|
17-Jul-2007 |
wenzelm <none@none> |
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
|
#
312bcb9e |
|
10-Jul-2007 |
wenzelm <none@none> |
simplified funpow, untabify;
|
#
c22948ec |
|
19-Jun-2007 |
wenzelm <none@none> |
moved balanced tree operations to General/balanced_tree.ML;
|
#
2fef31c0 |
|
05-Jun-2007 |
haftmann <none@none> |
moved generic algebra modules
|
#
a46fa2a0 |
|
03-Jun-2007 |
wenzelm <none@none> |
added flip (from General/basics.ML); renamed gen_submultiset to submultiset; moved downto0 to pattern.ML; moved legacy gen_merge_lists/merge_lists/merge_alists to Isar/locale.ML; moved plural to HOL/Tools/fundef_lib.ML; removed obsolete seq; simplified chop, fold2;
|
#
d16b574e |
|
02-Jun-2007 |
krauss <none@none> |
added "plural : 'a -> 'a -> 'b list -> 'a" for convenient error msg construction
|
#
782349c3 |
|
04-Apr-2007 |
paulson <none@none> |
find_first is just an alias
|
#
ec9c6a17 |
|
03-Apr-2007 |
wenzelm <none@none> |
removed obsolete scanwords (see obsolete tactic.ML:rename_tac for its only use);
|
#
3df4ae13 |
|
03-Apr-2007 |
wenzelm <none@none> |
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
|
#
13753020 |
|
27-Feb-2007 |
wenzelm <none@none> |
gensym: removed bits of dead code;
|
#
7a2d3541 |
|
27-Feb-2007 |
paulson <none@none> |
gensym no longer includes ' or _ in names (trailing _ is bad)
|
#
1f461ef6 |
|
06-Feb-2007 |
berghofe <none@none> |
Made untabify function tail recursive.
|
#
9ae7511f |
|
21-Jan-2007 |
nipkow <none@none> |
Added lists-as-multisets functions
|
#
9946f056 |
|
30-Dec-2006 |
wenzelm <none@none> |
removed conditional combinator;
|
#
01e1c7ab |
|
29-Dec-2006 |
wenzelm <none@none> |
added signed_string_of_int (pruduces proper - instead of SML's ~);
|
#
f1e8a838 |
|
28-Dec-2006 |
wenzelm <none@none> |
removed nospaces (Char.isSpace does not conform to Isabelle conventions);
|
#
a2550d04 |
|
22-Dec-2006 |
paulson <none@none> |
string primtives
|
#
c77312d9 |
|
14-Dec-2006 |
wenzelm <none@none> |
tuned -- accomodate Alice;
|
#
89015704 |
|
27-Nov-2006 |
wenzelm <none@none> |
simplified '?' operator;
|
#
0dc46c18 |
|
22-Nov-2006 |
wenzelm <none@none> |
moved string_of_pair/list/option to structure ML_Syntax;
|
#
2da4825c |
|
15-Nov-2006 |
wenzelm <none@none> |
moved some fundamental concepts to General/basics.ML;
|
#
2b809872 |
|
13-Nov-2006 |
haftmann <none@none> |
added higher-order combinators for structured results
|
#
a8c1bbaa |
|
05-Nov-2006 |
wenzelm <none@none> |
removed obsolete first_duplicate;
|
#
47420a1c |
|
31-Oct-2006 |
haftmann <none@none> |
cleanup
|
#
ea4e499c |
|
11-Oct-2006 |
haftmann <none@none> |
abandoned findrep
|
#
cfcb3b9c |
|
10-Oct-2006 |
haftmann <none@none> |
gen_rem(s) abandoned in favour of remove / subtract
|
#
654bfe4f |
|
06-Oct-2006 |
wenzelm <none@none> |
added the_single;
|
#
178591c2 |
|
04-Oct-2006 |
haftmann <none@none> |
insert replacing ins ins_int ins_string
|
#
d7f28396 |
|
11-Sep-2006 |
wenzelm <none@none> |
tuned eq_list;
|
#
7317a1ce |
|
31-Aug-2006 |
paulson <none@none> |
Empty is better than Match
|
#
08b261b8 |
|
08-Aug-2006 |
haftmann <none@none> |
abandoned equal_list in favor for eq_list
|
#
ecae7b18 |
|
17-Jul-2006 |
webertj <none@none> |
butlast removed (use fst o split_last instead)
|
#
b09d79c1 |
|
15-Jul-2006 |
webertj <none@none> |
function butlast added
|
#
1a8c37be |
|
12-Jul-2006 |
haftmann <none@none> |
added chop_prefix
|
#
a554dcaf |
|
11-Jul-2006 |
wenzelm <none@none> |
replaced read_radixint by read_intinf;
|
#
5240a185 |
|
04-Jul-2006 |
wenzelm <none@none> |
removed parrot comment;
|
#
ac58e9b6 |
|
03-Jul-2006 |
webertj <none@none> |
comment added
|
#
7cfb8fb3 |
|
06-Jun-2006 |
wenzelm <none@none> |
added zip_options;
|
#
8fcd20f8 |
|
20-May-2006 |
wenzelm <none@none> |
removed obsolete partition (cf. List.partition); tuned;
|
#
c28d14bb |
|
16-May-2006 |
wenzelm <none@none> |
added divide_and_conquer combinator (by Amine Chaieb); removed remains of old option type; removed obsolete eq_opt; removed obsolete string_of_bool (use Bool.toString instead); tuned;
|
#
129181dd |
|
09-May-2006 |
haftmann <none@none> |
removed superfluous eq_ord
|
#
bdd2d7de |
|
07-May-2006 |
webertj <none@none> |
string_of_option tuned
|
#
c1053ce4 |
|
05-May-2006 |
webertj <none@none> |
string_of_... functions added
|
#
b59205ed |
|
02-May-2006 |
wenzelm <none@none> |
sys_error: exception SYS_ERROR;
|
#
88ac89dc |
|
30-Apr-2006 |
wenzelm <none@none> |
added serial_string;
|
#
030616cf |
|
27-Apr-2006 |
wenzelm <none@none> |
renamed mapfilter to map_filter, made pervasive (again); made flat pervasive (again); added maps;
|
#
bfb768b3 |
|
26-Apr-2006 |
wenzelm <none@none> |
removed splitAt (superceded by chop); removed if_none (superceded by the_default);
|
#
25ac9520 |
|
25-Apr-2006 |
wenzelm <none@none> |
made 'flat' pervasive (again);
|
#
67f2fb67 |
|
24-Apr-2006 |
haftmann <none@none> |
moved coalesce to AList, added equality predicates to library
|
#
b17b4534 |
|
12-Apr-2006 |
wenzelm <none@none> |
export unflat (again);
|
#
24c80f59 |
|
09-Apr-2006 |
wenzelm <none@none> |
added coalesce;
|
#
2eb88a65 |
|
20-Mar-2006 |
wenzelm <none@none> |
added subtract; tuned;
|
#
6290c888 |
|
14-Mar-2006 |
wenzelm <none@none> |
added singleton;
|
#
20f2bc8b |
|
10-Mar-2006 |
haftmann <none@none> |
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
|
#
f405b21a |
|
22-Feb-2006 |
haftmann <none@none> |
abandoned merge_alists' in favour of generic AList.merge
|
#
be108470 |
|
15-Feb-2006 |
wenzelm <none@none> |
removed distinct, renamed gen_distinct to distinct;
|
#
09138719 |
|
11-Feb-2006 |
wenzelm <none@none> |
added chop (sane version of splitAt); added prefixes, suffixes;
|
#
51f4aa18 |
|
09-Feb-2006 |
wenzelm <none@none> |
tuned;
|
#
4ce51b74 |
|
07-Feb-2006 |
wenzelm <none@none> |
removed eq-polymorphic duplicates; renamed gen_duplicates to duplicates; added is_equal;
|
#
d43c0d7a |
|
03-Feb-2006 |
wenzelm <none@none> |
removed obsolete gen_ins/mem; added merge -- supercedes gen_merge_lists';
|
#
cd764178 |
|
19-Jan-2006 |
wenzelm <none@none> |
tuned setmp;
|
#
d4616777 |
|
14-Jan-2006 |
wenzelm <none@none> |
added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all; added transform_failure; added prefix;
|
#
09511ead |
|
03-Jan-2006 |
haftmann <none@none> |
rearranged burrow_split to fold_burrow to allow composition with fold_map
|
#
475973da |
|
27-Dec-2005 |
haftmann <none@none> |
added map_index
|
#
d0069466 |
|
21-Dec-2005 |
wenzelm <none@none> |
tuned;
|
#
8bffd7bc |
|
21-Dec-2005 |
haftmann <none@none> |
added eq_ord
|
#
42d4efbe |
|
21-Dec-2005 |
haftmann <none@none> |
discontinued unflat in favour of burrow and burrow_split
|
#
7047b6bf |
|
20-Dec-2005 |
haftmann <none@none> |
removed infix prefix, introduces burrow
|
#
6289a449 |
|
16-Dec-2005 |
wenzelm <none@none> |
added sort_distinct; removed obsolete unique_strings;
|
#
2fc76bf0 |
|
08-Dec-2005 |
wenzelm <none@none> |
tuned;
|
#
91976aa9 |
|
06-Dec-2005 |
haftmann <none@none> |
added 'dig' combinator
|
#
b5cbb92c |
|
02-Dec-2005 |
haftmann <none@none> |
added perhaps option combinator
|
#
c4391a83 |
|
02-Dec-2005 |
haftmann <none@none> |
introduced new map2, fold
|
#
b6f7af03 |
|
29-Nov-2005 |
wenzelm <none@none> |
added nth_list;
|
#
a37cd830 |
|
28-Nov-2005 |
haftmann <none@none> |
added (curried) fold2
|
#
f33b0187 |
|
10-Nov-2005 |
wenzelm <none@none> |
curried multiply;
|
#
66f1c965 |
|
31-Oct-2005 |
haftmann <none@none> |
fold_index replacing foldln
|
#
67bf68ad |
|
28-Oct-2005 |
haftmann <none@none> |
cleaned up nth, nth_update, nth_map and nth_string functions
|
#
c74e8e01 |
|
21-Oct-2005 |
haftmann <none@none> |
abandoned rational number functions in favor of General/rat.ML
|
#
857bcc5f |
|
11-Oct-2005 |
wenzelm <none@none> |
moved string_of_pid to ML-Systems;
|
#
68daf615 |
|
10-Oct-2005 |
paulson <none@none> |
small tidy-up of utility functions
|
#
db589537 |
|
04-Oct-2005 |
wenzelm <none@none> |
minor tweaks for Poplog/ML;
|
#
7c807c1f |
|
21-Sep-2005 |
wenzelm <none@none> |
tuned;
|
#
2c89f682 |
|
21-Sep-2005 |
haftmann <none@none> |
removed assoc, overwrite
|
#
47f92dcc |
|
20-Sep-2005 |
haftmann <none@none> |
improved eq_fst and eq_snd, removed some deprecated stuff
|
#
09285158 |
|
19-Sep-2005 |
haftmann <none@none> |
removed some deprecated assocation list functions
|
#
e97ecb2f |
|
13-Sep-2005 |
wenzelm <none@none> |
added exception EXCEPTION of exn * string;
|
#
a7de20c5 |
|
08-Sep-2005 |
haftmann <none@none> |
added the_list, the_default
|
#
2d2e2ab6 |
|
05-Sep-2005 |
haftmann <none@none> |
introduced binding priority 1 for linear combinators etc.
|
#
d3e15337 |
|
28-Aug-2005 |
haftmann <none@none> |
added 'these', removed assoc2
|
#
69554dba |
|
25-Aug-2005 |
haftmann <none@none> |
added ? combinator for conditional transformations
|
#
802db7c2 |
|
18-Aug-2005 |
wenzelm <none@none> |
added tap;
|
#
e2623f56 |
|
16-Aug-2005 |
wenzelm <none@none> |
tuned unsuffix/unprefix;
|
#
b9b77941 |
|
07-Aug-2005 |
nipkow <none@none> |
fixed typo in ratadd
|
#
722c1ccf |
|
06-Aug-2005 |
nipkow <none@none> |
added more rat functions
|
#
2aaea514 |
|
01-Aug-2005 |
wenzelm <none@none> |
tuned dict_ord;
|
#
6647b942 |
|
19-Jul-2005 |
wenzelm <none@none> |
added has_duplicates; tuned qsort;
|
#
2ea8c061 |
|
18-Jul-2005 |
haftmann <none@none> |
reverted from fold_yield to fold_map
|
#
1dbd51e6 |
|
14-Jul-2005 |
wenzelm <none@none> |
tuned;
|
#
86a859d1 |
|
14-Jul-2005 |
haftmann <none@none> |
added ` combinator
|
#
b2cde16b |
|
12-Jul-2005 |
haftmann <none@none> |
fold_map -> fold_yield, added transformator combinators, added selector combinator
|
#
16942bfa |
|
06-Jul-2005 |
wenzelm <none@none> |
tuned;
|
#
ffebc6ba |
|
06-Jul-2005 |
wenzelm <none@none> |
tuned;
|
#
886621b0 |
|
05-Jul-2005 |
wenzelm <none@none> |
tuned K;
|
#
2990d6bf |
|
05-Jul-2005 |
haftmann <none@none> |
added combinatros '||>' and '||>>' and fold_map fitting nicely to ST combinator '|->'
|
#
d9ae5035 |
|
05-Jul-2005 |
haftmann <none@none> |
added ST combinator '|->'
|
#
e7618cc5 |
|
04-Jul-2005 |
wenzelm <none@none> |
added fast_string_ord;
|
#
b0654bf5 |
|
01-Jul-2005 |
wenzelm <none@none> |
low-level tuning of fold, fold_rev, foldl_map;
|
#
00a35928 |
|
22-Jun-2005 |
wenzelm <none@none> |
added structure Object (from Pure/General/object.ML);
|
#
dae871e9 |
|
20-Jun-2005 |
wenzelm <none@none> |
added member, option_ord;
|
#
aaa9a50f |
|
17-Jun-2005 |
wenzelm <none@none> |
added serial numbers;
|
#
17d2b789 |
|
02-Jun-2005 |
wenzelm <none@none> |
replaced foldl_string by fold_string; added forall_string; improved unsuffix/unprefix: no explode;
|
#
56105db3 |
|
31-May-2005 |
wenzelm <none@none> |
export filter; remove: generalized type;
|
#
e39d75a6 |
|
17-May-2005 |
wenzelm <none@none> |
removed rev_append; tuned presentation of datatype option: removed apsome, export the and if_none;
|
#
f2340401 |
|
16-May-2005 |
paulson <none@none> |
Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
|
#
98fa49d2 |
|
17-Apr-2005 |
wenzelm <none@none> |
clarified insert/remove; tuned canonical fold/fold_rev;
|
#
7ab1abde |
|
16-Apr-2005 |
wenzelm <none@none> |
added gen_remove, remove; usual arrangement BasicLibrary: BASIC_LIBRARY and Library: LIBRARY;
|
#
50933e3d |
|
10-Apr-2005 |
ballarin <none@none> |
First release of interpretation commands.
|
#
70dede39 |
|
07-Apr-2005 |
wenzelm <none@none> |
invalidated former constructors None/OPTION to prevent accidental use as match-all patterns!
|
#
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
8988881a |
|
26-Oct-2004 |
berghofe <none@none> |
Added function merge_alists'.
|
#
74b36bb3 |
|
19-Jul-2004 |
berghofe <none@none> |
Added function unprefix.
|
#
1d9e1a7c |
|
16-Jul-2004 |
wenzelm <none@none> |
int_ord = Int.compare, string_ord = String.compare;
|
#
d8fc3665 |
|
11-Jul-2004 |
wenzelm <none@none> |
added fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b;
|
#
33b1b845 |
|
21-Jun-2004 |
kleing <none@none> |
Merged in license change from Isabelle2004
|
#
ac920ae4 |
|
18-Jun-2004 |
wenzelm <none@none> |
tuned exists_string;
|
#
07ee8b93 |
|
12-Jun-2004 |
wenzelm <none@none> |
added translate_string;
|
#
f02b7d74 |
|
05-Jun-2004 |
wenzelm <none@none> |
tuned exeption handling (capture/release);
|
#
66ab595f |
|
29-May-2004 |
wenzelm <none@none> |
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
|
#
c6d69b1f |
|
21-May-2004 |
berghofe <none@none> |
- exported result datatype - added functions get_result and get_exn
|
#
e20f9237 |
|
21-May-2004 |
wenzelm <none@none> |
added fold, product; removed transitive_closure;
|
#
889ec004 |
|
17-Apr-2004 |
berghofe <none@none> |
Fixed bug in rmod that caused an overflow exception in SML/NJ.
|
#
b504e110 |
|
19-Mar-2004 |
paulson <none@none> |
Removing the datatype declaration of "order" allows the standard General.order to be used. Thus we can use Int.compare and String.compare instead of the slower home-grown versions.
|
#
47837739 |
|
11-Jul-2003 |
berghofe <none@none> |
Added several functions for producing random numbers.
|
#
6f764b31 |
|
29-Jan-2003 |
berghofe <none@none> |
Added function rev_append.
|
#
e424867a |
|
07-Oct-2002 |
nipkow <none@none> |
take/drop -> splitAt
|
#
b23a3b2b |
|
08-Aug-2002 |
wenzelm <none@none> |
transform_error: pass through Interrupt;
|
#
fc3df123 |
|
19-Feb-2002 |
wenzelm <none@none> |
removed obscure functions bump_int_list, bump_list, bump_string;
|
#
3581f7bb |
|
17-Jan-2002 |
wenzelm <none@none> |
added timeap_msg;
|
#
75026064 |
|
08-Dec-2001 |
wenzelm <none@none> |
export writeln_default; tuned prefix_lines;
|
#
99af4abd |
|
03-Dec-2001 |
wenzelm <none@none> |
removed questionable init_gensym;
|
#
4073a400 |
|
26-Nov-2001 |
wenzelm <none@none> |
clarified order in gen_merge_lists';
|
#
031b629a |
|
24-Nov-2001 |
wenzelm <none@none> |
added gen_merge_lists(') and merge_lists('); removed obsolete generic_extend, generic_merge, extend_list;
|
#
11ea0df9 |
|
20-Nov-2001 |
wenzelm <none@none> |
added tracing, tracing_fn;
|
#
44ba4b08 |
|
20-Nov-2001 |
wenzelm <none@none> |
added prefixes1, suffixes1;
|
#
40eec31e |
|
11-Nov-2001 |
wenzelm <none@none> |
added unflat;
|
#
0a297cc3 |
|
20-Oct-2001 |
wenzelm <none@none> |
conditional: bool -> (unit -> unit) -> unit; std_error: string -> unit;
|
#
54da0609 |
|
15-Oct-2001 |
wenzelm <none@none> |
map_nth_elem;
|
#
fdf863b7 |
|
31-Aug-2001 |
berghofe <none@none> |
Added function unique_strings.
|
#
d67a5a04 |
|
01-Feb-2001 |
wenzelm <none@none> |
comment
|
#
b585794a |
|
30-Jan-2001 |
oheimb <none@none> |
added foldln
|
#
7948dcd3 |
|
21-Jan-2001 |
wenzelm <none@none> |
added replicate_string;
|
#
185b437d |
|
18-Dec-2000 |
nipkow <none@none> |
added rational arithmetic
|
#
f1d307e1 |
|
04-Sep-2000 |
wenzelm <none@none> |
tuned;
|
#
9f074ce8 |
|
31-Aug-2000 |
wenzelm <none@none> |
added priority, priority_fn;
|
#
53155ca0 |
|
29-Aug-2000 |
nipkow <none@none> |
*** empty log message ***
|
#
1ffec831 |
|
25-Jun-2000 |
wenzelm <none@none> |
added change: 'a ref -> ('a -> 'a) -> unit;
|
#
30d6b9a6 |
|
30-May-2000 |
wenzelm <none@none> |
global timing flag;
|
#
9d1fc842 |
|
05-May-2000 |
wenzelm <none@none> |
GPLed;
|
#
3601fd97 |
|
12-Mar-2000 |
wenzelm <none@none> |
added |>> and |>>>;
|
#
79bf5229 |
|
01-Dec-1999 |
paulson <none@none> |
fixed the discrepancy in the ordering of the constructors LESS EQUAL GREATER (for Moscow ML)
|
#
ec9ad13e |
|
05-Oct-1999 |
wenzelm <none@none> |
added untabify;
|
#
5f44310d |
|
04-Sep-1999 |
wenzelm <none@none> |
equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool;
|
#
efc40f99 |
|
27-Jul-1999 |
paulson <none@none> |
added gen_inter
|
#
4b8308b0 |
|
10-Jul-1999 |
wenzelm <none@none> |
try/can: pass Interrupt and ERROR; nth_elem_string: use try;
|
#
8340e17c |
|
12-May-1999 |
wenzelm <none@none> |
strip_quotes replaced by unenclose;
|
#
aa6d0601 |
|
27-Apr-1999 |
wenzelm <none@none> |
added oooo;
|
#
03ccec36 |
|
08-Mar-1999 |
wenzelm <none@none> |
added nth_elem_string, exists_string;
|
#
48957b28 |
|
13-Feb-1999 |
wenzelm <none@none> |
foldl_string;
|
#
5bf490fc |
|
25-Nov-1998 |
wenzelm <none@none> |
removed prs / prs_fn (broken, because it did not include \n in its semantics, forcing writeln to add one uncoditionally); replaced prs_fn by writeln fn;
|
#
ef2ec022 |
|
24-Nov-1998 |
wenzelm <none@none> |
fixed prefix_lines: *separate* by \n;
|
#
f7838087 |
|
20-Nov-1998 |
wenzelm <none@none> |
std_output, prefix_lines;
|
#
c04d3307 |
|
17-Nov-1998 |
wenzelm <none@none> |
val apply: ('a -> 'a) list -> 'a -> 'a; val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b;
|
#
69c192ec |
|
16-Nov-1998 |
wenzelm <none@none> |
added oo, ooo (*concatenation: 2 and 3 args*);
|
#
e0660736 |
|
10-Aug-1998 |
wenzelm <none@none> |
val single: 'a -> 'a list; val suffix: string -> string -> string; val unsuffix: string -> string -> string;
|
#
74805982 |
|
02-Jul-1998 |
wenzelm <none@none> |
Symbol.beginning;
|
#
3a254794 |
|
15-Jun-1998 |
wenzelm <none@none> |
handle_error: capture error msgs, even if no exception raised;
|
#
48dd03be |
|
05-Jun-1998 |
wenzelm <none@none> |
removed type object (see object.ML);
|
#
0da02724 |
|
25-May-1998 |
wenzelm <none@none> |
added foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list; added seq2: ('a * 'b -> unit) -> 'a list * 'b list -> unit; tuned 'beginning';
|
#
d24a9479 |
|
19-May-1998 |
wenzelm <none@none> |
fixed handle_error: cat_lines;
|
#
6b6956e8 |
|
13-May-1998 |
wenzelm <none@none> |
added transform_error, exception ERROR_MESSAGE;
|
#
571cd2c3 |
|
12-May-1998 |
wenzelm <none@none> |
get_first: ('a -> 'b option) -> 'a list -> 'b option;
|
#
8898f482 |
|
04-May-1998 |
wenzelm <none@none> |
added nth_update: 'a -> int * 'a list -> 'a list;
|
#
0243a664 |
|
29-Apr-1998 |
wenzelm <none@none> |
tuned error msgs;
|
#
870997ac |
|
03-Apr-1998 |
wenzelm <none@none> |
type_error;
|
#
98b56688 |
|
10-Mar-1998 |
nipkow <none@none> |
New simplifier flag for mutual simplification.
|
#
3ab759a3 |
|
09-Mar-1998 |
wenzelm <none@none> |
added merge_alists; moced is_letter etc. to Syntax/symbol.ML;
|
#
b33c0f7e |
|
18-Feb-1998 |
wenzelm <none@none> |
tuned comment;
|
#
7f3dd005 |
|
13-Feb-1998 |
wenzelm <none@none> |
added append (curried);
|
#
f8db05d2 |
|
12-Feb-1998 |
wenzelm <none@none> |
added explicit signature; improved comments;
|
#
93f80b7c |
|
11-Feb-1998 |
wenzelm <none@none> |
improved is_letter etc.;
|
#
c06a95b9 |
|
29-Dec-1997 |
wenzelm <none@none> |
removed distinct_fst_string;
|
#
9cedcb66 |
|
23-Dec-1997 |
wenzelm <none@none> |
improved comment;
|
#
d4935805 |
|
19-Dec-1997 |
wenzelm <none@none> |
added rev_order, make_ord; reimplemented sort function: stable version of quicksort;
|
#
10a42275 |
|
04-Dec-1997 |
wenzelm <none@none> |
added eq_set;
|
#
884ca074 |
|
01-Dec-1997 |
wenzelm <none@none> |
added prod_ord, dict_ord, list_ord;
|
#
163be543 |
|
28-Nov-1997 |
paulson <none@none> |
New timing functions startTiming and endTiming
|
#
b123381e |
|
26-Nov-1997 |
wenzelm <none@none> |
removed merge_opts;
|
#
2f3f1066 |
|
20-Nov-1997 |
wenzelm <none@none> |
added type object = exn;
|
#
a02123ba |
|
19-Nov-1997 |
wenzelm <none@none> |
added get_error: 'a error -> string option, get_ok: 'a error -> 'a option; added multiply: 'a list * 'a list list -> 'a list list;
|
#
a2b21e03 |
|
13-Nov-1997 |
wenzelm <none@none> |
made SML/NJ happy;
|
#
1e1c62bd |
|
12-Nov-1997 |
wenzelm <none@none> |
major cleanup; removed several obsolete functions; moved file stuff to Thy/file.ML;
|
#
9f62fae9 |
|
10-Nov-1997 |
oheimb <none@none> |
polished definition of find_index_eq
|
#
a9ea8fb9 |
|
07-Nov-1997 |
oheimb <none@none> |
changed libraray function find to find_index_eq, currying it
|
#
e4707da3 |
|
06-Nov-1997 |
wenzelm <none@none> |
tuned;
|
#
2a76c5e9 |
|
05-Nov-1997 |
wenzelm <none@none> |
fixed exception OPTION; added try, can;
|
#
6d73aac0 |
|
03-Nov-1997 |
wenzelm <none@none> |
added distinct_fst_string;
|
#
f5b1b2ae |
|
01-Nov-1997 |
paulson <none@none> |
Faster lexing
|
#
32c8a8fd |
|
30-Oct-1997 |
wenzelm <none@none> |
added merge_opts: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option;
|
#
a90c77c9 |
|
22-Oct-1997 |
wenzelm <none@none> |
added sort_wrt;
|
#
836d17e7 |
|
15-Oct-1997 |
wenzelm <none@none> |
tuned comment;
|
#
74ad0f2c |
|
10-Oct-1997 |
wenzelm <none@none> |
fixed space_explode, old one retained as BAD_space_explode; added split_lines;
|
#
2feda3c8 |
|
01-Oct-1997 |
wenzelm <none@none> |
added split_last;
|
#
566665fb |
|
23-Sep-1997 |
wenzelm <none@none> |
added handle_error: ('a -> 'b) -> 'a -> 'b error;
|
#
076d1818 |
|
08-Aug-1997 |
wenzelm <none@none> |
added append_file;
|
#
eee6b5b3 |
|
06-Aug-1997 |
wenzelm <none@none> |
added read_file, write_file;
|
#
ec2efc1b |
|
05-Aug-1997 |
berghofe <none@none> |
Added function "file_exists".
|
#
5f1e78e1 |
|
22-Jul-1997 |
wenzelm <none@none> |
added error_msg;
|
#
c691cdfb |
|
18-Jul-1997 |
wenzelm <none@none> |
improved output channels: normal, warning, error;
|
#
1ec8bd00 |
|
05-Jun-1997 |
paulson <none@none> |
Removal of radixstring from string_of_int; addition of string_of_indexname
|
#
84f72501 |
|
03-Jun-1997 |
wenzelm <none@none> |
is_blank: fixed space2;
|
#
7e034960 |
|
30-May-1997 |
paulson <none@none> |
flushOut ensures that no recent error message are lost (not certain this is necessary)
|
#
79fa8013 |
|
20-May-1997 |
paulson <none@none> |
Declares Option_ as synonym for structure Option
|
#
8f588e84 |
|
29-Apr-1997 |
wenzelm <none@none> |
is_blank: added space2 (160);
|
#
a2b68f54 |
|
17-Apr-1997 |
wenzelm <none@none> |
renamed set_ap to setmp;
|
#
54b4de3a |
|
16-Apr-1997 |
wenzelm <none@none> |
improved inc, dec; added set_ap;
|
#
1b7af086 |
|
18-Mar-1997 |
paulson <none@none> |
gensym no longer generates random identifiers, but just enumerates them starting from A. The random number generator was needlessly slow and caused portability problems.
|
#
2ae56b38 |
|
17-Jan-1997 |
wenzelm <none@none> |
added gen_overwrite;
|
#
54db31ec |
|
13-Jan-1997 |
wenzelm <none@none> |
added datatype order;
|
#
cd78fcd2 |
|
06-Jan-1997 |
wenzelm <none@none> |
added stamp util;
|
#
1716ee19 |
|
16-Dec-1996 |
wenzelm <none@none> |
fixed comment;
|
#
11c6be03 |
|
05-Dec-1996 |
wenzelm <none@none> |
added pwd;
|
#
f4bd2fa6 |
|
03-Dec-1996 |
paulson <none@none> |
Random number generated "downgraded" to generate numbers below 2^29 - 1, for MLWorks compatibility
|
#
cbff28d6 |
|
27-Nov-1996 |
paulson <none@none> |
Declares List_ as a synonym for List
|
#
8767c38d |
|
27-Nov-1996 |
paulson <none@none> |
Eta-expanded some declarations that are illegal under value polymorphism Converted I/O operatios for Basis Library compatibility
|
#
355c8bfd |
|
18-Nov-1996 |
wenzelm <none@none> |
added is_printable: string -> bool;
|
#
b57eae9d |
|
13-Nov-1996 |
paulson <none@none> |
Removal of polymorphic equality via mem, subset, eq_set, etc
|
#
31e0dfd5 |
|
12-Nov-1996 |
paulson <none@none> |
Updated syntax; shortened comments; put in monomorphic versions of ins
|
#
80e3a5a8 |
|
04-Nov-1996 |
paulson <none@none> |
Removal of now unused sum, max, min. Use foldl op+, Int.max, Int.min
|
#
c1e3f08c |
|
25-Sep-1996 |
paulson <none@none> |
Prevention of Overflow exception (for SML/NJ) in gensym
|
#
c97e793c |
|
23-Sep-1996 |
paulson <none@none> |
Addition of gensym
|
#
0324ad34 |
|
28-Mar-1996 |
berghofe <none@none> |
Added functions pr_latex and printgoal_latex which display current proof state in xdvi window
|
#
bd3d197b |
|
20-Mar-1996 |
paulson <none@none> |
maketest now closes the output file Declared type mtree for proof objects
|
#
ef87df96 |
|
14-Mar-1996 |
berghofe <none@none> |
Added some functions which allow redirection of Isabelle's output
|
#
79b79e6d |
|
14-Mar-1996 |
berghofe <none@none> |
Added some optimized versions of functions dealing with sets (i.e. mem, ins, eq_set etc.) which do not use the polymorphic = operator
|
#
ecb6e3c2 |
|
29-Jan-1996 |
clasohm <none@none> |
inserted tabs again
|
#
385672e0 |
|
29-Jan-1996 |
clasohm <none@none> |
removed tabs
|
#
ec2c6db7 |
|
29-Jan-1996 |
clasohm <none@none> |
added absolute_path
|
#
7a790ca7 |
|
17-Dec-1995 |
clasohm <none@none> |
added subdir_of
|
#
019b23ec |
|
22-Nov-1995 |
clasohm <none@none> |
files now define a structure to allow SML/NJ to optimize the code
|
#
e3bb6ed3 |
|
24-Oct-1995 |
clasohm <none@none> |
added space_explode and relative_path
|
#
02aae368 |
|
15-Mar-1995 |
lcp <none@none> |
Declares the function exit_use to behave like use but fail if errors are detected. It can be used in all Makefiles except Pure, which will write the exception handler explicitly ("exit" will have been declared already).
|
#
93644bda |
|
18-Aug-1994 |
lcp <none@none> |
Pure/library/assert_all: new, moved from ZF/ind_syntax.ML
|
#
736c52c2 |
|
12-Aug-1994 |
lcp <none@none> |
Pure/library/enclose, Pure/Syntax/pretty/enclose: renamed from parents Pure/library/is_blank: now handles form feeds () too, in accordance with ML definition
|
#
294e562e |
|
01-Jun-1994 |
wenzelm <none@none> |
replaced infix also by |>
|
#
78d1dfb6 |
|
19-May-1994 |
wenzelm <none@none> |
added infix op also: 'a * ('a -> 'b) -> 'b; added set, reset, toggle: bool ref -> bool; added find_first, exists2, forall2, commas_quote, merge_rev_lists;
|
#
3b4b1bcd |
|
08-Feb-1994 |
wenzelm <none@none> |
added eq_set;
|
#
9f70aab5 |
|
03-Feb-1994 |
wenzelm <none@none> |
added if_none, parents, commas, gen_duplicates, duplicates, assoc2; changed cat_lines: no final "\n";
|
#
a94a6ac1 |
|
19-Jan-1994 |
nipkow <none@none> |
removed square and fact
|
#
3bda4310 |
|
19-Jan-1994 |
wenzelm <none@none> |
major cleanup and reorganisation; added generic_extend, generic_merge; added various minor functions;
|
#
8440a255 |
|
29-Dec-1993 |
wenzelm <none@none> |
added sys_error;
|
#
2718a162 |
|
30-Nov-1993 |
wenzelm <none@none> |
changed split_filename, remove_ext; added base_name;
|
#
740ad6e7 |
|
29-Nov-1993 |
wenzelm <none@none> |
added equal, not_equal: ''a -> ''a -> bool
|
#
786aee8e |
|
07-Oct-1993 |
wenzelm <none@none> |
added cons, rcons, last_elem, sort_strings, take_suffix; improved tack_on;
|
#
7f03ab67 |
|
05-Oct-1993 |
clasohm <none@none> |
added functions that operate on filenames: split_filename (originally located in Pure/read.ML), tack_on, remove_ext
|
#
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|