tuned antiquotation theory;

value restriction

removed old cygwin wrappers;

declare_constraints: reset constraint on dummyS;

removed Isar/isar_thy.ML;

added dummyS;

removed legacy read/cert/string_of; removed obsolete IsarThy.theorem_i; tuned comments;

recdef_tc(_i): local_theory interface via Specification.theorem_i; incorporated IsarThy into IsarCmd;

incorporated IsarThy into IsarCmd;

removed theorem(_i); incorporated into IsarCmd;

upd

atbroy51 broke down, switch to atbroy9

updated

antiquotation "theory": proper output, only check via ThyInfo.theory;

tuned;

added antiquotation @{theory name};

fixed comment -- oops;

adjusted to new fun''

*** empty log message ***

added antiquotation theory

cleaned up

added theory antiquotation

combinator for overwriting changes with warning

added higher-order combinators for structured results

adjusted name in generated code

dropped LOrder dependency

moved upwars in HOL theory graph

added thy dependencies

PreList = Main - List

introduces preorders

dropped Inductive dependency

dropped Typedef dependency

added LOrder dependency

tuned ml antiquotations

adjusted

tuned

added tt tag

auto_term => lexicographic_order

updated

replaced "auto_term" by the simpler method "relation", which does not try to simplify. Some more cleanup.

added fresh_prodD, which is included fresh_prodD into mksimps setup;

added lexicographic_order.ML to makefile

image_constant_conv no longer [simp]

instantiate: tuned indentity case;

removed dead code;

mk_atomize: careful matching against rules admits overloading;

started reorgnization of lattice theories

Added in is_fol_thms.

level: do not account for local theory blocks (relevant for document preparation);

local 'end': no default tags; tag parser: do not swallow trailing newlines;

* Local theory targets ``context/locale/class ... begin'' followed by ``end''.

removed obsolete context;

turned 'context' into plain thy_decl, discontinued thy_switch;

tuned proofs;

updated local theory targets; removed 'context' as theory switch;

updated local theory targets; added 'context' as local theory switch; tuned;

updated;

Update standard keyword files.

tuned comments; back to fast String.compare (almost no difference in performance);

tuned comments;

tuned names of start_timing,/end_timing/check_timer; removed obsolete ML compatibility fragments;

removed obsolete ML compatibility fragments;

avoid strange typing problem in MosML;

tuned names of start_timing,/end_timing/check_timer;

simplified local theory wrappers;

removed mapping; added reinit;

simplified exit; added reinit;

simplified LocalTheory.exit;

Improvement to classrel clauses: now outputs the minimum needed. Theorem names: trying to minimize the number of multiple theorem names presented

deleted all uses of sign_of as it's now the identity function

tuned;

tuned Variable.trade;

introduces canonical AList functions for loop_tacs

minor refinements

redundancy checkes includes eta-expansion

improved syntax

added bounded_linear and bounded_bilinear locales

no special treatment for cygwin (this is supposed to be actual cygwin, not win32 polyml within cygwin);

tuned comments;

added x86-cygwin;

oracle raises CooperDec.COOPER instead of COOPER (this is eliminated). Erronous old behaviour due to this exception is now correcrted.

LocalTheory.restore;

init: '-' refers to global context; provide reinit operation;

abbrevs: return result; LocalTheory.restore;

Stack.map_top;

abbrevs: return result; separate reinit/restore;

separate map_top/all;

abbrevs: return result (use LocalTheory.abbrevs directly);

tuned;

abbrevs: return result;

timing/tracing code removed

interpreters for fst and snd added

new CCS-based implementation that should work with PolyML 5.0

HOL: less/less_eq on bool, modified syntax;

removed obsolete locale_results;

tuned;

imports Binimial;

updated;

lfp_induct_set;

modified less/less_eq syntax to avoid "x < y < z" etc.;

added lemma mult_mono'

added LIM_norm and related lemmas

moved theories Parity, GCD, Binomial to Library;

added profiling code, improved handling of proof terms, generation of domain introduction rules becomes optional (global reference FundefCommon.domintros)

incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;

case_tr': proper handling of authentic consts;

removed obsolete nat_case_tr' (duplicates case_tr' in datatype_package.ML);

renamed DatatypeHooks.invoke to all

moved lemma eq_neq_eq_imp_neq to HOL

renamed Lattice_Locales to Lattices

abstract ordering theories

obsolete (cf. ROOT.ML);