2006-11-12 wenzelm 2006-11-12 removed dead code;
2006-11-12 wenzelm 2006-11-12 mk_atomize: careful matching against rules admits overloading;
2006-11-12 nipkow 2006-11-12 started reorgnization of lattice theories
2006-11-11 mengj 2006-11-11 Added in is_fol_thms.
2006-11-11 wenzelm 2006-11-11 level: do not account for local theory blocks (relevant for document preparation);
2006-11-11 wenzelm 2006-11-11 local 'end': no default tags; tag parser: do not swallow trailing newlines;
2006-11-11 wenzelm 2006-11-11 * Local theory targets ``context/locale/class ... begin'' followed by ``end''.
2006-11-11 wenzelm 2006-11-11 removed obsolete context;
2006-11-11 wenzelm 2006-11-11 turned 'context' into plain thy_decl, discontinued thy_switch;
2006-11-11 wenzelm 2006-11-11 tuned proofs;
2006-11-11 wenzelm 2006-11-11 updated local theory targets; removed 'context' as theory switch;
2006-11-11 wenzelm 2006-11-11 updated local theory targets; added 'context' as local theory switch; tuned;
2006-11-11 wenzelm 2006-11-11 updated;
2006-11-11 wenzelm 2006-11-11 Update standard keyword files.
2006-11-10 wenzelm 2006-11-10 tuned comments; back to fast String.compare (almost no difference in performance);
2006-11-10 wenzelm 2006-11-10 tuned comments;
2006-11-10 wenzelm 2006-11-10 tuned names of start_timing,/end_timing/check_timer; removed obsolete ML compatibility fragments;
2006-11-10 wenzelm 2006-11-10 removed obsolete ML compatibility fragments;
2006-11-10 wenzelm 2006-11-10 avoid strange typing problem in MosML;
2006-11-10 wenzelm 2006-11-10 tuned names of start_timing,/end_timing/check_timer;
2006-11-10 wenzelm 2006-11-10 simplified local theory wrappers;
2006-11-10 wenzelm 2006-11-10 removed mapping; added reinit;
2006-11-10 wenzelm 2006-11-10 simplified exit; added reinit;
2006-11-10 wenzelm 2006-11-10 simplified LocalTheory.exit;
2006-11-10 paulson 2006-11-10 Improvement to classrel clauses: now outputs the minimum needed. Theorem names: trying to minimize the number of multiple theorem names presented
2006-11-10 urbanc 2006-11-10 deleted all uses of sign_of as it's now the identity function
2006-11-10 wenzelm 2006-11-10 tuned;
2006-11-10 wenzelm 2006-11-10 tuned Variable.trade;
2006-11-10 haftmann 2006-11-10 introduces canonical AList functions for loop_tacs
2006-11-10 haftmann 2006-11-10 minor refinements
2006-11-10 haftmann 2006-11-10 redundancy checkes includes eta-expansion
2006-11-10 haftmann 2006-11-10 improved syntax
2006-11-10 huffman 2006-11-10 added bounded_linear and bounded_bilinear locales
2006-11-10 wenzelm 2006-11-10 no special treatment for cygwin (this is supposed to be actual cygwin, not win32 polyml within cygwin);
2006-11-10 wenzelm 2006-11-10 tuned comments;
2006-11-09 wenzelm 2006-11-09 added x86-cygwin;
2006-11-09 chaieb 2006-11-09 oracle raises CooperDec.COOPER instead of COOPER (this is eliminated). Erronous old behaviour due to this exception is now correcrted.
2006-11-09 wenzelm 2006-11-09 LocalTheory.restore;
2006-11-09 wenzelm 2006-11-09 init: '-' refers to global context; provide reinit operation;
2006-11-09 wenzelm 2006-11-09 abbrevs: return result; LocalTheory.restore;
2006-11-09 wenzelm 2006-11-09 Stack.map_top;
2006-11-09 wenzelm 2006-11-09 abbrevs: return result; separate reinit/restore;
2006-11-09 wenzelm 2006-11-09 separate map_top/all;
2006-11-09 wenzelm 2006-11-09 abbrevs: return result (use LocalTheory.abbrevs directly);
2006-11-09 wenzelm 2006-11-09 tuned;
2006-11-09 wenzelm 2006-11-09 abbrevs: return result;
2006-11-09 webertj 2006-11-09 timing/tracing code removed
2006-11-09 webertj 2006-11-09 interpreters for fst and snd added
2006-11-09 webertj 2006-11-09 new CCS-based implementation that should work with PolyML 5.0
2006-11-09 wenzelm 2006-11-09 HOL: less/less_eq on bool, modified syntax;
2006-11-09 wenzelm 2006-11-09 removed obsolete locale_results;
2006-11-09 wenzelm 2006-11-09 tuned;
2006-11-09 wenzelm 2006-11-09 imports Binimial;
2006-11-09 wenzelm 2006-11-09 updated;
2006-11-09 wenzelm 2006-11-09 lfp_induct_set;
2006-11-09 wenzelm 2006-11-09 modified less/less_eq syntax to avoid "x < y < z" etc.;
2006-11-09 huffman 2006-11-09 added lemma mult_mono'
2006-11-09 huffman 2006-11-09 added LIM_norm and related lemmas
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;
2006-11-08 krauss 2006-11-08 added profiling code, improved handling of proof terms, generation of domain introduction rules becomes optional (global reference FundefCommon.domintros)