2008-03-28 haftmann 2008-03-28 unfold_locales now part of default tactic
2008-03-28 haftmann 2008-03-28 import Main explicitly
2008-03-28 haftmann 2008-03-28 dropped now superfluous ad-hoc adaption
2008-03-28 haftmann 2008-03-28 not depends on Main any longer
2008-03-28 haftmann 2008-03-28 accomodated to sledgehammer theory dependency requirement
2008-03-28 haftmann 2008-03-28 only invoke interpret
2008-03-28 wenzelm 2008-03-28 updated generated file;
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-28 wenzelm 2008-03-28 avoid rebinding of existing facts;
2008-03-28 haftmann 2008-03-28 some styling
2008-03-28 haftmann 2008-03-28 some styling
2008-03-28 haftmann 2008-03-28 some styling
2008-03-28 urbanc 2008-03-28 tuned proofs
2008-03-28 wenzelm 2008-03-28 tuned;
2008-03-28 wenzelm 2008-03-28 updated dependencies;
2008-03-28 wenzelm 2008-03-28 reorganized signature of ML_Context;
2008-03-27 huffman 2008-03-27 remove commented text
2008-03-27 wenzelm 2008-03-27 avoid ambiguity of State.state vs. JVMType.state;
2008-03-27 huffman 2008-03-27 declare cont_lemmas_ext as simp rules individually
2008-03-27 wenzelm 2008-03-27 avoid amiguity of Continuity.chain vs. Porder.chain;
2008-03-27 wenzelm 2008-03-27 avoid amiguity of State.state vs. JVMType.state;
2008-03-27 haftmann 2008-03-27 changed wrong assignement in signature sections
2008-03-27 haftmann 2008-03-27 clarified character serializations
2008-03-27 haftmann 2008-03-27 added Enum
2008-03-27 haftmann 2008-03-27 circumventing merge problem
2008-03-27 haftmann 2008-03-27 explicit case names for rule list_induct2
2008-03-27 haftmann 2008-03-27 instance for functions, explicit characters
2008-03-27 haftmann 2008-03-27 lemmas about map_of (zip _ _)
2008-03-27 haftmann 2008-03-27 restructuring; explicit case names for rule list_induct2
2008-03-27 haftmann 2008-03-27 no "attach UNIV" any more
2008-03-27 wenzelm 2008-03-27 tuned comments; tuned;
2008-03-27 wenzelm 2008-03-27 tuned comments;
2008-03-27 wenzelm 2008-03-27 fixed theory imports;
2008-03-27 wenzelm 2008-03-27 tuned appendix;
2008-03-27 wenzelm 2008-03-27 removed obsolete appl_syntax, applC_syntax;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-27 wenzelm 2008-03-27 Command 'setup': discontinued implicit version.
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure; renamed ML_Context.the_context to ML_Context.the_global_context;
2008-03-27 wenzelm 2008-03-27 renamed ML_Context.the_context to ML_Context.the_global_context; moved old the_context to old_goals.ML;
2008-03-27 wenzelm 2008-03-27 added process_file;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure; implicit setup of emerging theory Pure;
2008-03-27 wenzelm 2008-03-27 moved old the_context here; eliminated theory ProtoPure; renamed ML_Context.the_context to ML_Context.the_global_context;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure; implicit setup of emerging theory Pure; added >>> operator;
2008-03-27 wenzelm 2008-03-27 implicit setup of emerging theory Pure;
2008-03-27 wenzelm 2008-03-27 reduced to theory body (cf. OuterSyntax.process_file);
2008-03-27 wenzelm 2008-03-27 renamed ML_Context.the_context to ML_Context.the_global_context;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure;
2008-03-27 wenzelm 2008-03-27 removed Display.raw_string_of_XXX (use regular Sign.string_of_XXX);
2008-03-27 wenzelm 2008-03-27 HOL (and FOL): renamed variables in rules imp_elim and swap; Eliminated theory ProtoPure.
2008-03-27 wenzelm 2008-03-27 nonfix >>;
2008-03-27 huffman 2008-03-27 make preorder locale into a superclass of class po
2008-03-26 wenzelm 2008-03-26 removed obsolete Thy/thm_database.ML (cf. ML/ml_context.ML);
2008-03-26 wenzelm 2008-03-26 removed legacy ML bindings;
2008-03-26 wenzelm 2008-03-26 rule swap: renamed Pa to P;
2008-03-26 wenzelm 2008-03-26 added store_thms etc. (formerly in Thy/thm_database.ML); added bind_thm(s) (formerly in old_goals.ML); adapted to Context.thread_data interface; removed obsolete get/set_context; renamed ML_Context.>> to Context.>> (again);
2008-03-26 wenzelm 2008-03-26 adapted to Context.thread_data interface;
2008-03-26 wenzelm 2008-03-26 moved bind_thm(s) to ML/ml_context.ML; removed obsolete Thy/thm_database.ML (cf. ML/ml_context.ML);
2008-03-26 wenzelm 2008-03-26 added thread data (formerly global ref in ML/ml_context.ML); renamed ML_Context.>> to Context.>> (again);
2008-03-26 wenzelm 2008-03-26 pass imp_elim (instead of mp) and swap explicitly -- avoids store_thm;
2008-03-26 wenzelm 2008-03-26 pass imp_elim, swap to classical prover;