2012-10-01 wenzelm 2012-10-01 report sort assignment of visible type variables;
2012-10-01 wenzelm 2012-10-01 more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";
2012-10-01 blanchet 2012-10-01 fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)
2012-10-01 blanchet 2012-10-01 tweaked corecursor/coiterator tactic
2012-10-01 blanchet 2012-10-01 changed the type of the recursor for nested recursion
2012-09-30 blanchet 2012-09-30 fixed quick-and-dirty mode
2012-09-30 blanchet 2012-09-30 tuning
2012-09-30 traytel 2012-09-30 use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
2012-09-30 traytel 2012-09-30 got rid of subst_tac alias
2012-09-30 traytel 2012-09-30 tuned tactic
2012-09-29 wenzelm 2012-09-29 tuned proofs;
2012-09-29 wenzelm 2012-09-29 tuned proofs;
2012-09-29 wenzelm 2012-09-29 proper handling of constraints stemming from idtyp_ast_tr';
2012-09-29 wenzelm 2012-09-29 enable show_markup by default (approx. double output size);
2012-09-29 wenzelm 2012-09-29 more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-09-29 wenzelm 2012-09-29 explicit show_types takes preferenced over show_markup;
2012-09-29 wenzelm 2012-09-29 ignore wrapped markup elements in Proof General;
2012-09-29 wenzelm 2012-09-29 turn constraints into Isabelle_Markup.typing, depending on show_markup options; proper recursion in standard_format;
2012-09-29 wenzelm 2012-09-29 treat wrapped markup elements as raw markup delimiters;
2012-09-29 wenzelm 2012-09-29 tuned signature;
2012-09-28 wenzelm 2012-09-28 tuned proofs;
2012-09-28 wenzelm 2012-09-28 tuned proofs;
2012-09-28 wenzelm 2012-09-28 tuned proofs;
2012-09-28 wenzelm 2012-09-28 tuned;
2012-09-28 wenzelm 2012-09-28 support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
2012-09-28 wenzelm 2012-09-28 merged
2012-09-28 wenzelm 2012-09-28 eliminated dead code;
2012-09-28 wenzelm 2012-09-28 smarter handling of tracing messages;
2012-09-28 wenzelm 2012-09-28 display number of tracing messages;
2012-09-28 wenzelm 2012-09-28 tuned signature;
2012-09-28 wenzelm 2012-09-28 tuned proofs;
2012-09-28 blanchet 2012-09-28 simplified simpset
2012-09-28 blanchet 2012-09-28 fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
2012-09-28 traytel 2012-09-28 tuned tactic
2012-09-28 wenzelm 2012-09-28 updated keywords using proper "isabelle update_keywords";
2012-09-28 traytel 2012-09-28 tuned tactic
2012-09-28 traytel 2012-09-28 tuned tactic
2012-09-28 blanchet 2012-09-28 merge
2012-09-28 blanchet 2012-09-28 renamed ML file in preparation for next step
2012-09-28 blanchet 2012-09-28 killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"
2012-09-28 blanchet 2012-09-28 modernized example, exploiting "rep_compat" option
2012-09-28 blanchet 2012-09-28 compatibility option to use "rep_datatype"
2012-09-28 blanchet 2012-09-28 tuned message
2012-09-28 blanchet 2012-09-28 modernized example
2012-09-28 traytel 2012-09-28 tuned tactics
2012-09-28 nipkow 2012-09-28 second usage of const_typ
2012-09-28 nipkow 2012-09-28 new antiquotation const_typ
2012-09-28 nipkow 2012-09-28 tuned printing of _ in latex
2012-09-27 kuncar 2012-09-27 mk_readable_rsp_thm_eq is more robust now
2012-09-27 kuncar 2012-09-27 new get function for non-symmetric relator_eq & tuned
2012-09-27 wenzelm 2012-09-27 merged
2012-09-27 traytel 2012-09-27 tuned tactic; got rid of substs_tac alias
2012-09-27 blanchet 2012-09-27 use a nicer scheme to indexify names
2012-09-27 traytel 2012-09-27 tuned tactic
2012-09-27 traytel 2012-09-27 type of the bound of a BNF depends at most on dead type variables
2012-09-27 blanchet 2012-09-27 repaired signature
2012-09-27 blanchet 2012-09-27 lower the defaults for the number of bits, based on an example by Lukas Bulwahn
2012-09-27 blanchet 2012-09-27 modernized examples
2012-09-27 nipkow 2012-09-27 merged
2012-09-27 nipkow 2012-09-27 tuned