2008-04-08 krauss 2008-04-08 Generic conversion and tactic "atomize_elim" to convert elimination rules to the object logic
2008-04-08 wenzelm 2008-04-08 obsolete;
2008-04-08 wenzelm 2008-04-08 removed isatool expandshort; added isatool yxml;
2008-04-08 wenzelm 2008-04-08 removed obsolete AUTO_BASH feature;
2008-04-08 wenzelm 2008-04-08 removed obsolete AUTO_PERL feature;
2008-04-08 wenzelm 2008-04-08 support for YXML notation -- XML done right;
2008-04-08 wenzelm 2008-04-08 support "YXML" mode for output transfer notation; tuned;
2008-04-08 kleing 2008-04-08 removed abbrev for word_power. Was in the wrong direction and unused.
2008-04-07 wenzelm 2008-04-07 prefer plain ASCII here;
2008-04-07 wenzelm 2008-04-07 abs_conv: extra argument for bound variable; renamed iterated forall_conv to params_conv; added forall_conv, implies_conv, implies_concl_conv, rewr_conv;
2008-04-07 wenzelm 2008-04-07 added swap_params;
2008-04-07 wenzelm 2008-04-07 abs_conv: extra argument for bound variable;
2008-04-07 wenzelm 2008-04-07 renamed iterated forall_conv to params_conv;
2008-04-07 haftmann 2008-04-07 instantiation replacing primitive instance plus overloaded defs; more conservative type arities
2008-04-07 haftmann 2008-04-07 instantiation replacing primitive instance plus overloaded defs
2008-04-07 haftmann 2008-04-07 instantiation replacing primitive instance plus overloaded defs; realpow.simps now named power_real.simps
2008-04-07 haftmann 2008-04-07 explicit definition for "/"
2008-04-07 haftmann 2008-04-07 explicit dummy instantiation for div
2008-04-07 paulson 2008-04-07 * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
2008-04-07 paulson 2008-04-07 Superficial changes CVS: ----------------------------------------------------------------------
2008-04-04 haftmann 2008-04-04 tuned
2008-04-04 haftmann 2008-04-04 syntactic classes for bit operations
2008-04-04 haftmann 2008-04-04 renamed app2 to map2
2008-04-04 haftmann 2008-04-04 more new primrec
2008-04-04 haftmann 2008-04-04 prefix for equations in primrec specifications
2008-04-04 haftmann 2008-04-04 postprocessing of equality
2008-04-03 wenzelm 2008-04-03 parser: use plain explode, not Symbol.explode!
2008-04-03 wenzelm 2008-04-03 removed obsolete add_axiomss(_i);
2008-04-03 wenzelm 2008-04-03 renamed XML.parse_comment_whspc to XML.parse_comments;
2008-04-03 wenzelm 2008-04-03 renamed parse_comment_whspc to parse_comments; major parser cleanup -- removed junk comments;
2008-04-03 wenzelm 2008-04-03 removed yxmlN for now; moved test_markup to proof_general_emacs.ML; use efficient YXML markup internally (output, markup, message); message: issue MALFORMED MESSAGE explicitly; tuned;
2008-04-03 wenzelm 2008-04-03 moved test_markup here;
2008-04-03 wenzelm 2008-04-03 further cleanup of XML signature;
2008-04-03 wenzelm 2008-04-03 tuned comments;
2008-04-03 wenzelm 2008-04-03 further cleanup of XML signature; replaced plain_content by incremental add_content; added stream output;
2008-04-03 wenzelm 2008-04-03 output: canonical argument order (as opposed to write);
2008-04-03 wenzelm 2008-04-03 XML.string_of;
2008-04-03 wenzelm 2008-04-03 moved output_markup to xml.ML; added yxmlN mode name;
2008-04-03 wenzelm 2008-04-03 XML.output_markup;
2008-04-03 wenzelm 2008-04-03 XML.string_of, XML.parse;
2008-04-03 wenzelm 2008-04-03 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.; added output_markup, parse_element; detect: check XY; tuned comments; tuned;
2008-04-03 wenzelm 2008-04-03 added output_markup (from Tools/isabelle_process.ML); major cleanup of signature;
2008-04-03 wenzelm 2008-04-03 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
2008-04-03 wenzelm 2008-04-03 tuned comments;
2008-04-03 berghofe 2008-04-03 Added skip_mono flag to inductive definition package.
2008-04-03 berghofe 2008-04-03 Added skip_mono flag to inductive definition package.
2008-04-03 berghofe 2008-04-03 Added skip_mono flag and inductive_flags type.
2008-04-03 berghofe 2008-04-03 Deleted code for axiomatic introduction of datatypes. Instead, the package now uses SkipProof.prove rather than Goal.prove to do proofs.
2008-04-03 berghofe 2008-04-03 Removed QuickAndDirty constructor from simproc_dist datatype.
2008-04-03 berghofe 2008-04-03 - use SkipProof.prove_global instead of Goal.prove_global - added skip_mono flag to inductive definition package
2008-04-03 berghofe 2008-04-03 Added prove_global.
2008-04-03 krauss 2008-04-03 Function package no longer overwrites theorems. Some tuning.
2008-04-03 wenzelm 2008-04-03 Why XML notation?
2008-04-03 wenzelm 2008-04-03 Symbol.STX, Symbol.DEL;
2008-04-03 wenzelm 2008-04-03 Symbol.SOH;
2008-04-03 wenzelm 2008-04-03 added detect; removed auxiliary buffer_of_tree; tuned;
2008-04-03 wenzelm 2008-04-03 added some ASCII control symbols;
2008-04-03 wenzelm 2008-04-03 added Pure/General/yxml.ML;
2008-04-03 urbanc 2008-04-03 added generalised definitions for freshness of sets of atoms and lists of atoms
2008-04-02 haftmann 2008-04-02 tuned imports