clarified signature;

clarified signature;

prefer tail-recursive version (despite 4b99b1214034);

tuned whitespace;

tuned (see map_index);

unused;

hexadecimal representation of byte string;

tuned signature: more operations;

clarified take/drop/chop prefix/suffix;

clarified signature;

clean log file on Windows;

use Poly/ML 5.7.1 test version as default;

store errors in build db;

permissive trim_line as in Scala, e.g. relevant for poly/TextIO.print output on Windows;

accomodate Poly/ML repository version, which treats singleton strings as boxed;

non-deprecated char literals for Scala

clarified modules;

clarified modules;
tuned signature;

discontinued cd, pwd;

clarified treatment of fragments of Isabelle symbols during bootstrap;

clarified modules;

clarified modules;

tuned;

clarified File.standard_path vs. File.platform_path (like Isabelle/Scala operations);
avoid patching of SML basis library;

tuned signature, in accordance to sortBy in Scala;

tuned;

obsolete;

separate module Random;
proper Synchronized.var;

renamed "pairself" to "apply2", in accordance to @{apply 2};

eliminated some exotic combinators;

tuned;

more compact representation of special string values;

tuned -- avoid confusion with @{assert} for system failures (exception Fail);

more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;

tuned messages -- in accordance to Isabelle/Scala;

support for nested text cartouches;
clarified Symbol.is_symbolic: exclude \<open> and \<close>;

combinator fold_range, corresponding to map_range

--HG--
extra : rebase_source : 00890a01bbaaeb8673d6cbaa55d2a6f454fbd7ff

more uniform Markup.print_real;

tuned signature -- prefer terminology of Scala and Axiom;

eliminated dead code;

tuned whitespace;

prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);

replaced quicksort by mergesort, which might be a bit more efficient for key operations like Ord_List.make, Sorts.minimize_sort;

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;

prefer explicitly qualified exception List.Empty;

discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);

moved some legacy stuff;

some support for grouped list operations;

tuned;

discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);

more abstract datatype stamp, which avoids pointless allocation of mutable cells;

more flexible sorting;
tuned display;

low-level tuning;

pervasive Basic_Library in Scala;
tuned;

getenv_strict in ML;
tuned;

old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;

more robust exception pattern General.Subscript;

slightly more special eq_list/eq_set, with shortcut involving pointer_eq;

smart_string_of_real: print integer values without fractional part;

made SML/NJ happy;

tuned string_of_int to avoid allocation for small integers;

standardized split_last/last_elem towards List.last;
eliminated obsolete Library.last_elem;

really fixed comment (cf. 7abeb749ae99)

fixing comment in library

removed confusing comments (cf. 500171e7aa59);

strict forall2

make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;

just one version of fold_rev2;

renamed raw "explode" function to "raw_explode" to emphasize its meaning;

added forall2 predicate lifter

tuned signatures;

discontinued obsolete function sys_error and exception SYS_ERROR;

support for real valued configuration options;

chop_while replace drop_while and take_while

take_while, drop_while

renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;

tuned;

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 =)

tuned white space;

take and drop as projections of chop

curried take/drop

--HG--
extra : rebase_source : 6e6b508d936640bef00f0ad0c4fb089ad5253ef0

avoid upto if not needed

made SML/NJ happy;

restored accidentally deleted submultiset

multiset operations with canonical argument order

map_range (and map_index) combinator

curried inter as canonical list operation (beware of argument order)

curried union as canonical list operation

removed old-style \ and \\ infixes

dropped redundant gen_ prefix

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

tuned/moved divide_and_conquer';

indicate CRITICAL nature of various setmp combinators;

Raw ML references as unsynchronized state variables.

added map_transpose

eliminated redundant Library.multiply;

dropped find_index_eq

funpow_yield; tuned

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;

made SML/NJ happy

renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);

Merge.

use long names for old-style fold combinators;

New command find_consts searching for constants by type (by Timothy Bourke).

Clarified comment.

clarified comment

removed legacy |>>>

burrow_fst

added change_result;

Thread.getLocal/setLocal;

replaced find_substring by first_field;

added find_substring;

removed obsolete untabify (superceded by SymbolPos.tabify_content);

changed wrong assignement in signature sections

tuned comments;

setmp: uninterruptible;

added surround;

added map_split

added setmp_thread_data;

removed separate exists/forall code;

serial: now based on specific version in structure Multithreading;

Added foldl1.

tuned signature;

map_product and fold_product

added bool_ord;

added yield_singleton

added perhaps_apply/loop;

removed obsolete flip;

added burrow_options;

added nth_drop

simplified type int (eliminated IntInf.int, integer);

added some int constraints (ML_Parse.fix_ints not active here);

named some CRITICAL sections;

added list update;

setmp: NAMED_CRITICAL;

moved exception capture/release to structure Exn;

eliminated transform_failure (to avoid critical section for main transactions);

added setmp_noncritical;
setmp: CRITICAL;

marked some CRITICAL sections (for multithreading);

added undefined: 'a -> 'b;

moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);

simplified funpow, untabify;

moved balanced tree operations to General/balanced_tree.ML;

moved generic algebra modules

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;

added "plural : 'a -> 'a -> 'b list -> 'a" for convenient error msg construction

find_first is just an alias

removed obsolete scanwords (see obsolete tactic.ML:rename_tac for its only use);

removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);

gensym: removed bits of dead code;

gensym no longer includes ' or _ in names (trailing _ is bad)

Made untabify function tail recursive.

Added lists-as-multisets functions

removed conditional combinator;

added signed_string_of_int (pruduces proper - instead of SML's ~);

removed nospaces (Char.isSpace does not conform to Isabelle conventions);

string primtives

tuned -- accomodate Alice;

simplified '?' operator;

moved string_of_pair/list/option to structure ML_Syntax;

moved some fundamental concepts to General/basics.ML;

added higher-order combinators for structured results

removed obsolete first_duplicate;

cleanup

abandoned findrep

gen_rem(s) abandoned in favour of remove / subtract

added the_single;

insert replacing ins ins_int ins_string

tuned eq_list;

Empty is better than Match

abandoned equal_list in favor for eq_list

butlast removed (use fst o split_last instead)

function butlast added

added chop_prefix

replaced read_radixint by read_intinf;

removed parrot comment;

comment added

added zip_options;

removed obsolete partition (cf. List.partition);
tuned;

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;

removed superfluous eq_ord

string_of_option tuned

string_of_... functions added

sys_error: exception SYS_ERROR;

added serial_string;

renamed mapfilter to map_filter, made pervasive (again);
made flat pervasive (again);
added maps;

removed splitAt (superceded by chop);
removed if_none (superceded by the_default);

made 'flat' pervasive (again);

moved coalesce to AList, added equality predicates to library

export unflat (again);

added coalesce;

added subtract;
tuned;

added singleton;

renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.

abandoned merge_alists' in favour of generic AList.merge

removed distinct, renamed gen_distinct to distinct;

added chop (sane version of splitAt);
added prefixes, suffixes;

tuned;

removed eq-polymorphic duplicates;
renamed gen_duplicates to duplicates;
added is_equal;

removed obsolete gen_ins/mem;
added merge -- supercedes gen_merge_lists';

tuned setmp;

added exception ERROR, error, cat_error, sys_error, assert, deny, assert_all;
added transform_failure;
added prefix;

rearranged burrow_split to fold_burrow to allow composition with fold_map

added map_index

tuned;

added eq_ord

discontinued unflat in favour of burrow and burrow_split

removed infix prefix, introduces burrow

added sort_distinct;
removed obsolete unique_strings;

tuned;

added 'dig' combinator

added perhaps option combinator

introduced new map2, fold

added nth_list;

added (curried) fold2

curried multiply;

fold_index replacing foldln

cleaned up nth, nth_update, nth_map and nth_string functions

abandoned rational number functions in favor of General/rat.ML

moved string_of_pid to ML-Systems;

small tidy-up of utility functions

minor tweaks for Poplog/ML;

tuned;

removed assoc, overwrite

improved eq_fst and eq_snd, removed some deprecated stuff

removed some deprecated assocation list functions

added exception EXCEPTION of exn * string;

added the_list, the_default

introduced binding priority 1 for linear combinators etc.

added 'these', removed assoc2

added ? combinator for conditional transformations

added tap;

tuned unsuffix/unprefix;

fixed typo in ratadd

added more rat functions

tuned dict_ord;

added has_duplicates;
tuned qsort;

reverted from fold_yield to fold_map

tuned;

added ` combinator

fold_map -> fold_yield, added transformator combinators, added selector combinator

tuned;

tuned;

tuned K;

added combinatros '||>' and '||>>' and fold_map fitting nicely to ST combinator '|->'

added ST combinator '|->'

added fast_string_ord;

low-level tuning of fold, fold_rev, foldl_map;

added structure Object (from Pure/General/object.ML);

added member, option_ord;

added serial numbers;

replaced foldl_string by fold_string;
added forall_string;
improved unsuffix/unprefix: no explode;

export filter;
remove: generalized type;

removed rev_append;
tuned presentation of datatype option: removed apsome, export the and if_none;

Use of IntInf.int instead of int in most numeric simprocs; avoids
integer overflow in SML/NJ

clarified insert/remove;
tuned canonical fold/fold_rev;

added gen_remove, remove;
usual arrangement BasicLibrary: BASIC_LIBRARY and Library: LIBRARY;

First release of interpretation commands.

invalidated former constructors None/OPTION to prevent accidental use as match-all patterns!

Move towards standard functions.

Deleted Library.option type.

Added function merge_alists'.

Added function unprefix.

int_ord = Int.compare, string_ord = String.compare;

added fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b;

Merged in license change from Isabelle2004

tuned exists_string;

added translate_string;

tuned exeption handling (capture/release);

output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;

- exported result datatype
- added functions get_result and get_exn

added fold, product; removed transitive_closure;

Fixed bug in rmod that caused an overflow exception in SML/NJ.

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.

Added several functions for producing random numbers.

Added function rev_append.

take/drop -> splitAt

transform_error: pass through Interrupt;

removed obscure functions bump_int_list, bump_list, bump_string;

added timeap_msg;

export writeln_default;
tuned prefix_lines;

removed questionable init_gensym;

clarified order in gen_merge_lists';

added gen_merge_lists(') and merge_lists(');
removed obsolete generic_extend, generic_merge, extend_list;

added tracing, tracing_fn;

added prefixes1, suffixes1;

added unflat;

conditional: bool -> (unit -> unit) -> unit;
std_error: string -> unit;

map_nth_elem;

Added function unique_strings.

comment

added foldln

added replicate_string;

added rational arithmetic

tuned;

added priority, priority_fn;

*** empty log message ***

added change: 'a ref -> ('a -> 'a) -> unit;

global timing flag;

GPLed;

added |>> and |>>>;

fixed the discrepancy in the ordering of the constructors LESS EQUAL GREATER
(for Moscow ML)

added untabify;

equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool;

added gen_inter

try/can: pass Interrupt and ERROR;
nth_elem_string: use try;

strip_quotes replaced by unenclose;

added oooo;

added nth_elem_string, exists_string;

foldl_string;

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;

fixed prefix_lines: *separate* by \n;

std_output, prefix_lines;

val apply: ('a -> 'a) list -> 'a -> 'a;
val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b;

added oo, ooo (*concatenation: 2 and 3 args*);

val single: 'a -> 'a list;
val suffix: string -> string -> string;
val unsuffix: string -> string -> string;

Symbol.beginning;

handle_error: capture error msgs, even if no exception raised;

removed type object (see object.ML);

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';

fixed handle_error: cat_lines;

added transform_error, exception ERROR_MESSAGE;

get_first: ('a -> 'b option) -> 'a list -> 'b option;

added nth_update: 'a -> int * 'a list -> 'a list;

tuned error msgs;

type_error;

New simplifier flag for mutual simplification.

added merge_alists;
moced is_letter etc. to Syntax/symbol.ML;

tuned comment;

added append (curried);

added explicit signature;
improved comments;

improved is_letter etc.;

removed distinct_fst_string;

improved comment;

added rev_order, make_ord;
reimplemented sort function: stable version of quicksort;

added eq_set;

added prod_ord, dict_ord, list_ord;

New timing functions startTiming and endTiming

removed merge_opts;

added type object = exn;

added get_error: 'a error -> string option, get_ok: 'a error -> 'a option;
added multiply: 'a list * 'a list list -> 'a list list;

made SML/NJ happy;

major cleanup;
removed several obsolete functions;
moved file stuff to Thy/file.ML;

polished definition of find_index_eq

changed libraray function find to find_index_eq, currying it

tuned;

fixed exception OPTION;
added try, can;

added distinct_fst_string;

Faster lexing

added merge_opts: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option;

added sort_wrt;

tuned comment;

fixed space_explode, old one retained as BAD_space_explode;
added split_lines;

added split_last;

added handle_error: ('a -> 'b) -> 'a -> 'b error;

added append_file;

added read_file, write_file;

Added function "file_exists".

added error_msg;

improved output channels: normal, warning, error;

Removal of radixstring from string_of_int; addition of string_of_indexname

is_blank: fixed space2;

flushOut ensures that no recent error message are lost (not certain this is
necessary)

Declares Option_ as synonym for structure Option

is_blank: added space2 (160);

renamed set_ap to setmp;

improved inc, dec;
added set_ap;

gensym no longer generates random identifiers, but just enumerates them
starting from A. The random number generator was needlessly slow and caused
portability problems.

added gen_overwrite;

added datatype order;

added stamp util;

fixed comment;

added pwd;

Random number generated "downgraded" to generate numbers below 2^29 - 1,
for MLWorks compatibility

Declares List_ as a synonym for List

Eta-expanded some declarations that are illegal under value polymorphism

Converted I/O operatios for Basis Library compatibility

added is_printable: string -> bool;

Removal of polymorphic equality via mem, subset, eq_set, etc

Updated syntax; shortened comments; put in monomorphic versions of ins

Removal of now unused sum, max, min. Use foldl op+, Int.max, Int.min

Prevention of Overflow exception (for SML/NJ) in gensym

Addition of gensym

Added functions pr_latex and printgoal_latex which
display current proof state in xdvi window

maketest now closes the output file
Declared type mtree for proof objects

Added some functions which allow redirection of Isabelle's output

Added some optimized versions of functions dealing with sets
(i.e. mem, ins, eq_set etc.) which do not use the polymorphic =
operator

inserted tabs again

removed tabs

added absolute_path

added subdir_of

files now define a structure to allow SML/NJ to optimize the code

added space_explode and relative_path

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).

Pure/library/assert_all: new, moved from ZF/ind_syntax.ML

Pure/library/enclose, Pure/Syntax/pretty/enclose: renamed from parents
Pure/library/is_blank: now handles form feeds () too, in accordance with
ML definition

replaced infix also by |>

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;

added eq_set;

added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
changed cat_lines: no final "\n";

removed square and fact

major cleanup and reorganisation;
added generic_extend, generic_merge;
added various minor functions;

added sys_error;

changed split_filename, remove_ext;
added base_name;

added equal, not_equal: ''a -> ''a -> bool

added cons, rcons, last_elem, sort_strings, take_suffix;
improved tack_on;

added functions that operate on filenames: split_filename (originally located
in Pure/read.ML), tack_on, remove_ext

Initial revision