Drule.merge_rules;

renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum

improvements for lazy code generation

fixed typo

added code generator serialization for Char

added notes on class_package.ML and codegen_package.ML

small adjustments

fixed bug for serialization for uminus on ints

small improvement in serialization for wfrec

added structure HOList

major simplifications for integers

tactic for prove_instance_arity now gets definition theorems as arguments

added term_of_string function

simplification for code generation for Integers

adaption to argument change in primrec_package

adaption to changes in class_package

hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen

exported equation transformator

class package and codegen refinements

added give_names and alphanum

Some cases in "case ... of ..." expressions may now be omitted (internally, these cases are assigned the "undefined" value).

- Added new "undefined" constant - normalization_conv no longer expects term to have form "Trueprop ..."

removed Variable.monomorphic;

comments fixed, member function renamed

Change to algebra method.

Reimplemented algebra method; now controlled by attribute.

Strict dfs traversal of imported and registered identifiers.

added map_default, internal restructuring

export is_tid;

thm_of_proof: improved generation of variables;

Sign.infer_types: Name.context; FactIndex.add_local: simplified interface; Variable.constraints_of;

reorganize declarations (more efficient); renamed rename_wrt to variant_frees (avoid confusion with Term.rename_wrt_term, which reverses the result); tuned;

Name.context for used'';

added variant_frees; tuned;

tuned;

export make_context, is_declared;

prove: Variable.declare_internal (more efficient);

add_local: simplified interface, all frees are known'';

Sign.infer_types: Name.context;

renamed Variable.rename_wrt to Variable.variant_frees;

Fixed the bugs introduced by the last commit! Output is now *identical* to that produced by the old version, based on a-lists.

MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems

thm_of_proof: tuned Name operations;

print_statement: tuned Variable operations;

added newly_fixed, focus; removed monomorphic; tuned;

added declare_term_names; tuned;

fold_proof_terms: canonical arguments; removed obsolete add_prf_names, add_prf_tfree_names, add_prf_tvar_ixns;

Term.declare_term_names;

Started implementing uniqueness proof for recursion combinator (still unfinished).

typo (theorerms) fixed

typo (theorerms) fixed

AList.join now with 'DUP' exception

added Table.map_default

removed obsolete ML files;

replaced butlast by Library.split_last;

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;