replaced butlast by Library.split_last; removed dead code;

butlast removed (use fst o split_last instead)

support for MiniSat proof traces added

support for MiniSat proof traces added

has_consts renamed to has_conn, now actually parses the first-order formula to avoid problems caused by connectives buried within descriptions and set comprehensions.

function butlast added

Replaced a-lists by tables to improve efficiency

Pass user lemmas' names to ResHolClause.tptp_write_file and dfg_write_file.

Only include combinators if required by goals and user specified lemmas. Remove a clause if too general.

Term.term_lpo takes order on terms rather than strings as argument.

keep/transaction: unified execution model (with debugging etc.); tuned;

trivial whitespace changes

simp method: depth_limit;

"conjecture" must be lower case

tuned insert_list;

Name.context already declares empty names; tune ins_sorts -- sort assigments should never change later;

strip_abs_eta: proper use of Name.context;

do not export make_context; initial context: declare empty names; variants: no special treatment of empty names;

removed colon from sym category;

fix to refl_clause_aux: added occurs check

* Isar: ":" (colon) is no longer a symbolic identifier character;

removed duplicate of Tactic.make_elim_preserve;

removed obsolete adhoc_freeze_vars (may use Variable.import_terms instead);

exported make_elim_preserve;

prove_conv: Variable.import_terms instead of Term.addhoc_freeze_vars; tuned;

simplified prove_conv;

removed ':' from category of symbolic identifier chars;

query/bang_colon: separate tokens;

purged website sources

added strip_abs_eta

added chop_prefix

class_of_param instead of class_of

adaptions in class_package

adaptions in codegen

variants: special treatment of empty name;

avoid reference to internal skolem;

separate names filed (covers fixes/defaults);

adapted Name.defaults_of;

removed obsolete xless; tuned zero_var_indexes;

clean: no special treatment of empty name; declare, invent: clean arguments;

removed obsolete xless;

replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes

uniform treatment of num/xnum; read_xnum: proper handling of bin/hex;

replaced read_radixint by read_intinf;

removed str_to_int in favour of general Syntax.read_xnum;

num/xnum: bin or hex;

Name.internal; Name.invent_list;

tuned;

* Pure: structure Name;

Names of basic logical entities (variables etc.).

replaced Term.variant(list) by Name.variant(_list); removed obsolete mem_term;

Name.internal; Name.dest_skolem;

adapted to more efficient Name/Variable implementation; removed dead code;

replaced Term.variant(list) by Name.variant(_list); Name.internal;

maintain Name.context for fixes/defaults; more efficient inventing/renaming of local names (cf. name.ML);

removed obsolete mem_ix;

removed obsolete ins_ix, mem_ix, ins_term, mem_term; moved variant(list), invent_names, bound, dest_internal/skolem etc. to name.ML;

Name.dest_skolem;

Name.bound;

replaced Term.variant(list) by Name.variant(_list); Name.bound;

replaced Term.variant(list) by Name.variant(_list); Name.invent_list;

replaced Term.variant(list) by Name.variant(_list); Name.clean;

Name.invent_list;

added name.ML;

Name.is_bound;

removed obsolete mem_term;

Name.internal;

replaced Term.variant(list) by Name.variant(_list);

let_simproc: activate Variable.import;

Witness theorems of interpretations now transfered to current theory.

New function transfer_witness lifting Thm.transfer to witnesses.

hex and binary numerals (contributed by Rafal Kolanski)

minor optimization wrt. certifying terms

tuned;

tuned;

updated;

tuned interface; case_ss: proper context;

tuned interface;

removed dead code;

Element.prove_witness: context; Goal.prove_global;

prove_witness: context;

tuned exception handling;

prove/prove_multi: context; prove_global: theory + standard; tuned;

simprocs: no theory argument -- use simpset context instead; misc cleanup;

distinct simproc/simpset: proper context;

presburger_ss: proper context;

presburger_ss: proper context; Goal.prove: context;

tuned;

avoid Force_tac, which uses a different context;

Goal.prove: context;

tactic/method simpset: maintain proper context;

Goal.prove_global; SkipProof.prove: context;

Goal.prove_global;

simprocs: no theory argument -- use simpset context instead; tuned interfaces;

simprocs: no theory argument -- use simpset context instead;

updated;

updated Goal.prove, Goal.prove_global;

added some bits on variables;

* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables; * Pure: Goal.prove, Goal.prove_global; tuned;

"solver" reference added to make the SAT solver configurable

Some tidying. Fixed a problem where the DFG file did not declare some TFrees as 0-ary functions. Frees no longer have types attached.

Fixed erroneous check-in.

made evaluation_conv and normalization_conv visible.

Internal restructuring: identify no longer computes syntax.

Modified comment.

added support for MiniSat 1.14

removed obsolete locale view;

apply_text: support Method.Source_i;

added method_i and Source_i;

thm parsers: include Args.internal_fact;

add/del_simps: warning for inactive simpset (no context); tuned;

updated;

Local variables;

Isar.context ();

tuned;

added Isar.context;

some tidying; fixed the output of theorem names

def_export: Drule.generalize;

matchers: fall back on plain first_order_matchers, not pattern;

make sure $DISTPREFIX exists before calling makedist

removed the "tagging" feature

made the conversion of elimination rules more robust

Literals aren't sorted any more.

Literals aren't sorted any more. Output overloaded constants' type var instantiations.

fixed let-simproc ----------------------------------------------------------------------

Isar: 'print_facts' prints all local facts;

print_lthms: include unnamed facts from index; tuned;

added content;