2012-09-28 ago wenzelm support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
2012-09-28 ago wenzelm merged
2012-09-28 ago wenzelm eliminated dead code;
2012-09-28 ago wenzelm smarter handling of tracing messages;
2012-09-28 ago wenzelm display number of tracing messages;
2012-09-28 ago wenzelm tuned signature;
2012-09-28 ago wenzelm tuned proofs;
2012-09-28 ago blanchet simplified simpset
2012-09-28 ago blanchet fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
2012-09-28 ago traytel tuned tactic
2012-09-28 ago wenzelm updated keywords using proper "isabelle update_keywords";
2012-09-28 ago traytel tuned tactic
2012-09-28 ago traytel tuned tactic
2012-09-28 ago blanchet merge
2012-09-28 ago blanchet renamed ML file in preparation for next step
2012-09-28 ago blanchet killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"
2012-09-28 ago blanchet modernized example, exploiting "rep_compat" option
2012-09-28 ago blanchet compatibility option to use "rep_datatype"
2012-09-28 ago blanchet tuned message
2012-09-28 ago blanchet modernized example
2012-09-28 ago traytel tuned tactics
2012-09-28 ago nipkow second usage of const_typ
2012-09-28 ago nipkow new antiquotation const_typ
2012-09-28 ago nipkow tuned printing of _ in latex
2012-09-27 ago kuncar mk_readable_rsp_thm_eq is more robust now
2012-09-27 ago kuncar new get function for non-symmetric relator_eq & tuned
2012-09-27 ago wenzelm merged
2012-09-27 ago traytel tuned tactic; got rid of substs_tac alias
2012-09-27 ago blanchet use a nicer scheme to indexify names
2012-09-27 ago traytel tuned tactic
2012-09-27 ago traytel type of the bound of a BNF depends at most on dead type variables
2012-09-27 ago blanchet repaired signature
2012-09-27 ago blanchet lower the defaults for the number of bits, based on an example by Lukas Bulwahn
2012-09-27 ago blanchet modernized examples
2012-09-27 ago nipkow merged
2012-09-27 ago nipkow tuned
2012-09-27 ago wenzelm operations to turn markup into XML;
2012-09-27 ago wenzelm removed obsolete org.w3c.dom operations;
2012-09-27 ago wenzelm eliminated obsolete HTML/CSS functionality;
2012-09-27 ago wenzelm removed obsolete Output1 dockable;
2012-09-27 ago wenzelm physical File.eq in conformance to Isabelle/ML;
2012-09-27 ago wenzelm tuned proofs;
2012-09-27 ago wenzelm tuned;
2012-09-27 ago wenzelm updated to consolidated SortedMap in scala-2.9.x;
2012-09-27 ago blanchet partly ported "TreeFI" example to new syntax
2012-09-27 ago blanchet avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
2012-09-27 ago nipkow tuned
2012-09-27 ago nipkow tuned
2012-09-27 ago blanchet merge
2012-09-27 ago blanchet modernized examples;
2012-09-26 ago wenzelm some support for jEdit warmstart;
2012-09-26 ago wenzelm discontinued XML.cache experiment -- Poly/ML 5.5.0 RTS does online sharing better;
2012-09-26 ago wenzelm tuned message;
2012-09-26 ago wenzelm merged
2012-09-26 ago blanchet disable parallel proofs for two big examples -- speeds up things and eliminates spurious Interrupt exceptions (to be investigated)
2012-09-26 ago blanchet got rid of other instance of shaky "Thm.generalize"
2012-09-26 ago blanchet tweaked theorem names (in particular, dropped s's)
2012-09-26 ago blanchet get rid of shaky "Thm.generalize"
2012-09-26 ago blanchet fixed "rels" + split them into injectivity and distinctness
2012-09-26 ago blanchet generate high-level "coinduct" and "strong_coinduct" properties