mainly new/different datatype examples

documentation updated

major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)

new default parameters for refute

solver "auto" now issues a warning when it uses solver "enumerate"

Corrected printer bug for bounded quantifiers Q x<=y. P

more group isomorphisms

added drop_take:thm

- deleted unneeded function eta_long (now in Pure/pattern.ML - added HOL.min / HOL.max to allowed consts again - added final simplification step with presburger_ss to preprocessor again

Adapted to new syntax for case expressions.

Added more flexible parse / print translations for case expressions.

Modified functions pt_to_ast and ast_to_term to improve handling of errors in parse (ast) translations caused by ambiguous input.

- exported result datatype - added functions get_result and get_exn

updated;

Pure: clear separation of logical types and nonterminals;

adapted tsig/sg interface;

added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;

added fold, product; removed transitive_closure;

adapted names of some sort ops;

major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;

Type.strip_sorts;

incorporate type inference interface from type.ML;

adapted tsig interface;

moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);

test_classrel/arity improve error reporting; tuned;

xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;

string_of_vname moved to term.ML;

incorporate sort ops from term.ML; use Graph.T; misc cleanup;

type.ML now before Syntax module;

xxx_typ_raw replace xxx_typ_no_norm forms;

'classrel' now allows multiple arguments;

Sign.certify_tyname;

TypeInfer.paramify_dummies, TypeInfer.param;

Args.local_typ_raw;

output_tym: removed duplicate clauses;

Graph.minimals;

adapted syntax to cope with lack of non-logical types;

Type.typ_instance;

load ML files only once;

removed duplicate thms;

Sign.typ_instance;

tuned message;

tuned document;

use plain SOME;

proper use of 'syntax';

auto update

has_consts now handles the @-operator

new bij_betw operator

more results about isomorphisms

conversion of Hilbert_Choice to Isar script

the function list1 has been exported.

A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.

tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger.

modified abel_cancel.ML for polymorphic types

simplification for abelian groups

Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy

Comments fixed

lemma disjoint_int_union removed - too special

Change of theory hierarchy: Group is now based in Lattice.

tidied

new atomize theorem

removed a premise of card_inj_on_le

removal of locale coset

deleted redundant proof lines

new lemmas

clauses for ordinary resolution

conversion of theorems to atomic form

New simp rules added: insert_disjoint disjoint_insert disjoint_int_union

simpilified and strengthened proofs

fixed latex problems

renamed `> to o_m

changes made due to new Ring_and_Field theory

Eta-expanded function scan_comment to make SmlNJ happy.

broken no longer includes TTP, and other minor changes

removal of prime characters

package needed for superscripts

conversion to clauses for ordinary resolution rather than ME

auto update

Pure: nested comments in inner syntax;

support nested comments;

changed Symbol.beginning;

tuned;

Source.of_list: no buffer limitation (now pointless due to tail-recursive Scan.repeat);

added Scan.list;

ProofGeneral.process_pgip command;

preparation for integration with new Ring_and_Field.thy

moved first lemma in LongDiv.ML to LongDiv.thy

replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style

removed Aux.thy;

cleanup up read functions, include liberal versions;

be liberal about constant names;

tuned;

tuned notation;

tuned document;

*** empty log message ***

Add FIXME note re FAIL (is it fixed yet?)

Add cdata output. Add tabs in whitespace. Write two strings instead of Library.quote.

Add -X option to trigger PGIP interaction mode.

*** empty log message ***

replaced Aux.thy by RealLemmas.thy

tuned HOL/record package; enabled record_upd_simproc by default.

improved block sup/sub;

show_structs option;

tuned document;

tidied

auto update

redundant clause removed

solved sml-nj compatibility problem

tuned;

reimplementation of HOL records; only one type is created for each record extension, instead of one type for each field. See NEWS.

tuned;

improvd indexed syntax and implicit structures; tuned renaming of symbolic identifiers

improved indexed syntax / implicit structures;

tuned;

improved Term.invent_names;

removed 'constdefs' hack;

improved syntax;

improved subscript syntax;

tuned instance statements;

_index1: accomodate improved indexed syntax;