Auxiliary functions to be used in generated code are now defined using "attach".

Implemented mechanism for attaching auxiliary code to consts_code and types_code declarations.

small text mod

Fixed some problems with the signal handler.

Improved implementation of Defs.is_overloaded.

Some changes to allow mutually recursive, overloaded functions with same name.

added Davenport reference

moved Davenport citation to Main, removed author list

moved gcd to new GCD.thy

proof needed updating because of arith

changed imports due to new GCD.thy

Used to be in Library/Primes

fix typo

replaced old continuity rules with new lemma cont2cont_lift_case

simplified proof of ifte_thms, removed ifte_simp

renamed upE1 to upE; added simp rule cont2cont_flift1

renamed upE1 to upE

define 'a u with datatype package; removed obsolete lemmas; renamed upE1 to upE and Exh_Up1 to Exh_Up; cleaned up

added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up

add lemma eq_sprod

add lemma eq_cprod

removed obsolete continuity theorems

define lift type using pcpodef; cleaned up

cleaned up

fixes to work with UU_reorient_simproc

fixes to work with UU_reorient_simproc

fixes to work with UU_reorient_simproc

1) all theorems in Orderings can now be given as a parameter 2) new function Theory.defs_of 3) new functions Defs.overloading_info and Defs.is_overloaded

use theorem ch2ch_cont

inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL

updated comment

add UU_reorient_simproc

use theorems ch2ch_cont, cont2contlubE

add lemmas ch2ch_cont and cont2contlubE

Preparations for interpretation of locales in locales.

takes & in premises apart now.

linear arithmetic is more powerful now

linear arithmetic now takes "&" in assumptions apart.

Used to be part of Finite_Set (or was it SetInterval?) Added binomial thm.

fixed antiquotation;

removed timers;

debug: exception_trace; tuned;

finish: Output.accumulated_time;

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'