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;