2006-01-05 urbanc 2006-01-05 changed the name of the type "nOption" to "noption".
2006-01-04 urbanc 2006-01-04 added "fresh_singleton" lemma
2006-01-04 urbanc 2006-01-04 added more documentation; will now try out a modification of the ok-predicate
2006-01-04 nipkow 2006-01-04 Reversed Larry's option/iff change.
2006-01-04 haftmann 2006-01-04 substantial additions using locales
2006-01-04 haftmann 2006-01-04 exported read|cert_arity interfaces
2006-01-04 nipkow 2006-01-04 trace_simp_depth_limit is 1 by default
2006-01-04 nipkow 2006-01-04 removed pointless trace msg.
2006-01-04 paulson 2006-01-04 preservation of names
2006-01-04 paulson 2006-01-04 a few more named lemmas
2006-01-04 haftmann 2006-01-04 fix: reintroduced pred_ctxt in gen_add_locale
2006-01-04 wenzelm 2006-01-04 tuned;
2006-01-04 wenzelm 2006-01-04 * Pure/Isar: Toplevel.theory_theory_to_proof;
2006-01-04 wenzelm 2006-01-04 added unlocalize_mfix;
2006-01-04 wenzelm 2006-01-04 added unlocalize_mixfix;
2006-01-04 wenzelm 2006-01-04 added theory_to_theory_to_proof, which may change theory before entering the proof; added forget_proof (from isar_thy.ML);
2006-01-04 wenzelm 2006-01-04 tuned;
2006-01-04 wenzelm 2006-01-04 moved forget_proof to toplevel.ML;
2006-01-04 wenzelm 2006-01-04 Toplevel.forget_proof;
2006-01-04 wenzelm 2006-01-04 adapted Toplevel.Proof;
2006-01-04 wenzelm 2006-01-04 removed dead code;
2006-01-04 wenzelm 2006-01-04 more stuff;
2006-01-03 paulson 2006-01-03 Provers/classical: stricter checks to ensure that supplied intro, dest and elim rules are well-formed
2006-01-03 paulson 2006-01-03 added explicit paths to required theories
2006-01-03 wenzelm 2006-01-03 added implementation manual;
2006-01-03 wenzelm 2006-01-03 more stuff;
2006-01-03 wenzelm 2006-01-03 fixed LaTeX source;
2006-01-03 haftmann 2006-01-03 class now a keyword
2006-01-03 haftmann 2006-01-03 class now an keyword, quoted where necessary
2006-01-03 haftmann 2006-01-03 add_local_context now yields imported and body elements seperatly; additional slight clenup in code
2006-01-03 haftmann 2006-01-03 rearranged burrow_split to fold_burrow to allow composition with fold_map
2006-01-03 wenzelm 2006-01-03 added unfolding(_i); renamed using_thmss(_i) to using_i;
2006-01-03 wenzelm 2006-01-03 unparse String/AltString: escape quotes;
2006-01-03 wenzelm 2006-01-03 tuned;
2006-01-03 wenzelm 2006-01-03 avoid hardwired Trueprop; local proof: static refererence to Pure.thy;
2006-01-03 wenzelm 2006-01-03 added 'using' command;
2006-01-03 wenzelm 2006-01-03 updated;
2006-01-03 wenzelm 2006-01-03 added IsarImplementation;
2006-01-03 wenzelm 2006-01-03 updated -- lost update!?
2006-01-03 wenzelm 2006-01-03 * Pure/Isar: new command 'unfolding'; * ML/Provers: more generic wrt. syntax of object-logics; tuned;
2006-01-02 wenzelm 2006-01-02 ISABELLE_USER for remote cvs access;
2006-01-02 wenzelm 2006-01-02 outline;
2006-01-02 wenzelm 2006-01-02 "The Isabelle/Isar Implementation" manual;
2005-12-31 wenzelm 2005-12-31 * Provers/classical: removed obsolete classical version of elim_format;
2005-12-31 wenzelm 2005-12-31 tuned forall_intr_vars;
2005-12-31 wenzelm 2005-12-31 added classical_rule, which replaces Data.make_elim; removed obsolete Data.make_elim and classical elim_format attribute; tuned;
2005-12-31 wenzelm 2005-12-31 explicitly reject consts *Goal*, *False*;
2005-12-31 wenzelm 2005-12-31 elim rules: Classical.classical_rule;
2005-12-31 wenzelm 2005-12-31 removed obsolete cla_dist_concl;
2005-12-31 wenzelm 2005-12-31 removed classical elim_format;
2005-12-31 wenzelm 2005-12-31 removed obsolete Provers/make_elim.ML;
2005-12-31 wenzelm 2005-12-31 obsolete, see classical_rule in Provers/classical.ML;
2005-12-31 wenzelm 2005-12-31 more robust phantomsection;
2005-12-30 wenzelm 2005-12-30 require cla_dist_concl, avoid assumptions about concrete syntax;
2005-12-30 wenzelm 2005-12-30 avoid implicit assumptions about consts Not, op =, *Goal*, *False*;
2005-12-30 wenzelm 2005-12-30 provide equality_name, not_name;
2005-12-30 wenzelm 2005-12-30 fixed final_consts;
2005-12-30 wenzelm 2005-12-30 provide cla_dist_concl;
2005-12-30 wenzelm 2005-12-30 non-PDF: phantomsection;
2005-12-29 haftmann 2005-12-29 added atom keyword