removed ad-hoc atp_hook, cal_atp; removed depth_of; tuned;

Toplevel.actual_proof;

avoid excessive exceptions;

Graph: fast_string_ord;

export eq_brl;

added subtract; improved interface; tuned;

export eq_rrule; improved Net interface;

removed obsolete delta stuff;

open ReconPrelim Recon_Transfer;

open ReconPrelim ReconTranslateProof; removed second copy of exception ASSERTION;

tuned;

use Toplevel.print_state_hook instead of adhoc Proof.atp_hook; added call_atp: bool ref; do 'setmp print_mode []', which is more robust than manual ref manipulation; added subtract_simpset, subtract_claset (supercede delta approximation);

tuned concat_with_and; improved Net interface;

improved Net interface;

* Isar session: The initial use of ROOT.ML is now always timed;

Add acceptedpgipelems message

auto update

generlization of some "nat" theorems

relevance filtering is now optional

tidied

fixed comment-out;

fix

Add management for current working directory

(fix for an accidental commit)

Note about theorem dependencies including themselves.

Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc

(intermediate commit)

(corrected wrong commit)

(intermediate commit)

- added cplex package to HOL/Matrix

avoid some garbage

- use TableFun instead of homebrew binary tree in am_interpreter.ML - add Floats to HOL/Real

- introduce Pure/Tools directory - add compute oracle to Pure/Tools

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

changed orientation of bind_assoc rule

use qualified names for all constants

added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined

generalized types of monadic operators to class cpo; added match function for UU

added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.) renamed simplification rules for abs (abs_of_pos, etc.) renamed rules for multiplication and signs (mult_pos_pos, etc.) moved lemmas involving fractions from NatSimprocs.thy added setsum_mono3 to FiniteSet.thy added simplification rules for powers to Parity.thy

experimental code to reduce the amount of type information in blast

tweaked

Added \<module> symbol.

Added "attach" keyword for code generator setup.

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;