dest_parsers: sort result;

added time_accumulator and accumulated_time supercede low-level time_info operations;

added full_prop_of: includes tpairs;

tuned eq_ix;

Context.check_thy;

tuned forall_elim_var(s): avoid expensive Term.add_vars;

tuned;

Thm.full_prop_of;

check_thy: less invocations, less verbose; tuned merge, merge_refs;

* Pure: Output.time_accumulator; * Isar toplevel: improved diagnostics;

isatool fixheaders;

tuned msg;

ThyInfo.time_use root;

added output_buffer;

added write_list, append_list;

tuned write: use File.write_list;

tuned maxidx;

tuned maxidx_of_typ/typs/term; moved adhoc string_of_term to HOL/Tools/ATP/recon_translate_proof.ML; cleaned signature;

multiple flags: prefer later ones;

use Symtab.table instead of ordered lists;

added adhoc string_of_term from Pure/term.ML;

removed term_lpo (now in Pure/term.ML);

tuned;

tuned;

changed file permissions;

changing file permissions ...

add keywords cpodef, pcpodef (for HOLCF)

renamed to Pcpodef.thy

use new pcpodef package

add pcpodef files

renamed from TypedefPcpo.thy; added theorems Rep_defined, Abs_defined; uses pcpodef_package.ML

new type definition package for HOLCF

simplified definitions of flift1, flift2, liftpair; added theorem cont2cont_flift1; renamed strictness and definedness theorems

tuned K;

fixed regexp grouping;

List.app; run both tests;

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

tuned;

* Pure: structure OrdList (cf. Pure/General/ord_list.ML); * Pure: more efficient orders for basic syntactic entities;

added ST combinator '|->'

Symtab: use fast_string_ord instead of string_ord -- affects order of Symtab.dest etc.;

tuned;

made smlnj happy;

methods: added simp_flags argument, added "depth_limit" flag;

added transform_exceptions: bool ref;

tuned;

dummy exception_trace;

tuned union: avoid garbage in trivial case;

dest_ctyp: raise exception for non-constructor; dest_comb: replaced expensive fastype_of by Term.argument_type; dest_abs: replaced expensive variant_abs by Term.dest_abs; hyps: fast_term_ord;

added fast_indexname_ord, fast_term_ord; changed sort_ord, typ_ord, Vartab, Termtab: use fast orders; added argument_type_of, dest_abs; tuned;

use fast_string_ord;

added fast_string_ord;

Streamlined the signal handler in watcher.ML

unified main and dist

started unifying main and dist

(intermediate commit)

Simple report generator for Poly/ML profiling output.

tuned;

ambig msg: warning again;

avoid polyeq;

tuned term_ord: less garbage;

cterm_aconv: avoid rep_cterm;

decomp_simp: compare terms, not cterms;

back to 1.28;

prime is a predicate now.

* Isar profiling: new reference Toplevel.profiling (default 0);

use tracing for potentially voluminous ambiguity output;

added profiler interface (dummy);

added profiler interface, keep 'profiling' of PolyML structure; removed PolyML.Compiler.printInAlphabeticalOrder := false;

added profile flag;

low-level tuning of map, fold;

ctyp: added 'sorts' field; may_insert_typ/term/env_sorts: observe Sign.all_sorts_nonempty; may_insert_env_sorts: insert sorts of type subst only; instantiate: insert sorts of insts; tuned;

added all_sorts_nonempty;

low-level tuning of fold, fold_rev, foldl_map;

isatool install: removed KDE option;

Fixed bug: lookup' must use = instead of eq_type to compare types of variables, otherwise pattern matching algorithm may loop.

Changed interface of Envir.lookup'

Moved eq_type from envir.ML to type.ML

Implemented modular code generation.

Simplified proof (thanks to strengthened ball_cong).

Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.

Adapted to new interface of RecfunCodegen.add.

Adapted to modular code generation.

Corrected implementation of arbitrary on cname.

Added BasisLibrary prefix to List.concat to avoid problems with modular code generation.

Moved code generator setup from NatBin to IntDef.

Simplified some proofs (thanks to strong_setsum_cong).

Removed setsubgoaler hack (thanks to strong_setsum_cong).

Removed setsubgoaler hack (thanks to strengthened finsum_cong).

Removed setsubgoaler hack.

Tuned finsum_cong to allow that premises are simplified more eagerly.

Added strong_ball_cong and strong_bex_cong (these are now the standard congruence rules for Ball and Bex).

Moved some code lemmas from Main to Nat.

Adapted to new interface of code generator.

Implemented trick (due to Tobias Nipkow) for fine-tuning simplification of premises of congruence rules.

Added strong_setsum_cong and strong_setprod_cong.

defaultsort pcpo

added theorem lift_definedE; moved cont_if to Cont.thy

added tactic cont_tac

remove uses of sign_of

cleaned up

cleaned up

renamed flatdom2monofun to flatdom_strict2mono

cleaned up; reorganized and added section headings

cleaned up; added adm_less to adm_lemmas; added subsection headings

revert to 1.27 due to obscure performance issues (!??);

replace filter2 with List.partition

Proper treatment of beta-redexes in witness theorems.

minor corrections

test sml-dev on mac as well

use only 1 CPU on MacOS 10.4.1

use kleing@cse instead of kleing@in.tum.de

use global settings for isatest-doc

export no_type_brackets; accomodate advanced trfuns; tuned;

proper treatment of advanced trfuns: pass thy argument; tuned warning;

transform_failure in translation functions: TRANSLATION_FAIL; proper treatment of advanced trfuns: pass thy argument; tuned bigimpl_ast_tr, impl_ast_tr';

proper treatment of advanced trfuns: pass thy argument; transform_failure in translation functions: TRANSLATION_FAIL; removed obsolete '*** INSUFFICIENT SYNTAX FOR PREFIX APPLICATION ***';

accomodate advanced trfuns;

removed obsolete (un)fold_ast2;

Drule.implies_intr_hyps;

added print': print depending on print_mode;

no Syntax.internal on thesis;

added print_mode three_buffersN and corresponding cond_print;

cond_print for end-of-proof and calculational commands;

added eq; improved copy/copy_dir: only copy if non-eq;

pass thy as explicit argument (the old ref was not safe in conjunction with lazy evaluation -- the unify code could be fooled about the present theory context);

more efficient treatment of shyps and hyps (use ordered lists); added 'sorts' field to cterm; removed obsolete fix_shyps; moved implies_intr_hyps to drule.ML;

Syntax.read thy;