Tests enforce proper export behaviour.

removed advanced recdef section and replaced it by citation of Alex's tutorial.

fix

no Gencode.ML

changed "treemap" example to "mirror"

added lemmas

replaced cc/ld phase by PolyML.SaveState.saveState (potentially more efficient);

removed obsolete ProofGeneral/parsing.ML;

activated new script parser;

Output.add_mode default prevents escapes from ProofGeneral mode;

added ProofGeneral/pgml_isabelle.ML;

the all-important ML antiquotations are back; tuned;

generic tactic Method.intros_tac

clarified theory target interface

more precise treatment of prove_subclass

proper reinitialisation after subclass

clarified

tweaked

recdef to fun

*** empty log message ***

Added reference to Jeremy Dawson's paper on the word library. Added header to remaining word/*.thy files so they show up in toc.

recdef -> fun

added Fun

tuned

recdef -> fun

*** empty log message ***

Catch exceptions arising during the abstraction operation. Filter out theorems that are "too deep".

Added example for the ideal membership problem solved by algebra

Added field ideal into entry - uses by algebra method to prove the ideal membership problem

changed signature according to normalizer_data.ML

tuned

(1) signatures updated according to normalizer_data.ML (added field ideal in entry); (2) For a theory the conversions returned are now ring_conv (as before, proves a universal statement), simple_ideal proves ideal membership for one polynomial ; multi_ideal solves the more general ideal membership for several existentially quantifier variables involved in several conjunctions; a simpset containing a simproc to turn x = y into p = 0 where p is the normal form of x - y; (3) Added ideal_tac a tactic to prove general ideal membership (cf. John Harrision CADE 2007) ; (4) Added algebra_tac : first tries ring_tac (old algebra) then ideal_tac

(1) added axiom to ringb and theorems to enable algebra to prove the ideal membership problem; (2) Method algebra now calls algebra_tac which first tries to solve a universal formula, then in case of failure trie to solve the ideal membership problem (see HOL/Tools/Groebner_Basis/groebner.ML)

exported field_comp_conv: a numerical conversion over fields

dropped AxClass

tuned

Handle Subscript exception when looking up bound variables.

Added well-formedness check to Abst case in function prf_of.

added omission

bugfixes concerning strange theorems

fixed typo

const antiquotation clarified

clarified

handling of notation in class target

fixed document preparation

improved website integration

adjusted

split library index into templates

split library index into templates

structured

tidied version

simplified proof

continued localization

fixed typo

added nbe

test_proof: do not change Proofterm.proofs here (not thread-safe);

improved notion of 'nicer' fact names (observe some name space properties);

export is_hidden;

added bool_ord;

qualified Proofterm.proofs;

fun/function: generate case names for induction rules

append/member: more light-weight way to declare authentic syntax; tuned proofs;

made SML/NJ happy;

safe_exit: controlled_execution;

better compute oracle

better compute oracle

adapted Compute...

use "fun" for definition of "member" -> authentic syntax

ASCIIfied README

added list comprehension syntax

locale_const: in_class workaround prevents additional locale version of class consts;

notation: associate syntax to checked-unchecked term;

export class_prefix; removed obsolete const hiding;

tuned

changed order of class parameters

dropped square syntax

localized monotonicity; tuned syntax

dropped "brown" syntax

replaced Secure.evaluate by ML_Context.evaluate;

asm_rewrite_goal_tac: avoiding PRIMITIVE lets informative exceptions (from simprocs) get through;

proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;

print the defined constants when finished; tuned

adjusted

tuned

added NEWS entry for function package

added hint for algebra

moved primitive operations to class.ML

fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.

dropped redundancy

various localizations

made command 'undo' silent ('ProofGeneral.undo' becomes a historical relic);

tuned

clarified implementation

propagation through class hierarchy

added function for evaluation by compiler invocation

more computation with rationals

localized further

continued

tuned

THIS_IS_ISABELLE_MAKEBIN;

updated;

README for polyml-5.1 binary distribution;

avoid very slow metis invocation (saves 1min on 1.60 GHz machine);

separate RecordPackage.timing flag;

tuned;

tuned file names etc.;

*** empty log message ***

added HOL-Statespace session;

be explicit about .ML files;

fixed HOL-Statespace for case-sensitive file-system;

tuned comments;

added Statespace library