2007-11-02 haftmann 2007-11-02 clarified theory target interface
2007-11-02 haftmann 2007-11-02 more precise treatment of prove_subclass
2007-11-02 haftmann 2007-11-02 proper reinitialisation after subclass
2007-11-02 haftmann 2007-11-02 clarified
2007-11-02 paulson 2007-11-02 tweaked
2007-11-02 paulson 2007-11-02 recdef to fun
2007-11-02 nipkow 2007-11-02 *** empty log message ***
2007-11-02 kleing 2007-11-02 Added reference to Jeremy Dawson's paper on the word library. Added header to remaining word/*.thy files so they show up in toc.
2007-11-02 nipkow 2007-11-02 recdef -> fun
2007-11-02 nipkow 2007-11-02 added Fun
2007-11-02 haftmann 2007-11-02 tuned
2007-11-01 nipkow 2007-11-01 recdef -> fun
2007-11-01 nipkow 2007-11-01 *** empty log message ***
2007-10-31 paulson 2007-10-31 Catch exceptions arising during the abstraction operation. Filter out theorems that are "too deep".
2007-10-31 chaieb 2007-10-31 Added example for the ideal membership problem solved by algebra
2007-10-31 chaieb 2007-10-31 Added field ideal into entry - uses by algebra method to prove the ideal membership problem
2007-10-31 chaieb 2007-10-31 changed signature according to normalizer_data.ML
2007-10-31 chaieb 2007-10-31 tuned
2007-10-31 chaieb 2007-10-31 (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
2007-10-31 chaieb 2007-10-31 (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)
2007-10-31 chaieb 2007-10-31 exported field_comp_conv: a numerical conversion over fields
2007-10-31 haftmann 2007-10-31 dropped AxClass
2007-10-31 haftmann 2007-10-31 tuned
2007-10-30 berghofe 2007-10-30 Handle Subscript exception when looking up bound variables.
2007-10-30 berghofe 2007-10-30 Added well-formedness check to Abst case in function prf_of.
2007-10-30 haftmann 2007-10-30 added omission
2007-10-30 paulson 2007-10-30 bugfixes concerning strange theorems
2007-10-30 haftmann 2007-10-30 fixed typo
2007-10-30 haftmann 2007-10-30 const antiquotation clarified
2007-10-30 haftmann 2007-10-30 clarified
2007-10-30 haftmann 2007-10-30 handling of notation in class target
2007-10-30 haftmann 2007-10-30 fixed document preparation
2007-10-30 haftmann 2007-10-30 improved website integration
2007-10-30 haftmann 2007-10-30 adjusted
2007-10-30 haftmann 2007-10-30 split library index into templates
2007-10-30 haftmann 2007-10-30 split library index into templates
2007-10-30 haftmann 2007-10-30 structured
2007-10-30 haftmann 2007-10-30 tidied version
2007-10-30 haftmann 2007-10-30 simplified proof
2007-10-30 haftmann 2007-10-30 continued localization
2007-10-29 haftmann 2007-10-29 fixed typo
2007-10-29 haftmann 2007-10-29 added nbe
2007-10-29 wenzelm 2007-10-29 test_proof: do not change Proofterm.proofs here (not thread-safe);
2007-10-29 wenzelm 2007-10-29 improved notion of 'nicer' fact names (observe some name space properties);
2007-10-29 wenzelm 2007-10-29 export is_hidden;
2007-10-29 wenzelm 2007-10-29 added bool_ord;
2007-10-29 wenzelm 2007-10-29 qualified Proofterm.proofs;
2007-10-29 krauss 2007-10-29 fun/function: generate case names for induction rules
2007-10-28 wenzelm 2007-10-28 append/member: more light-weight way to declare authentic syntax; tuned proofs;
2007-10-28 wenzelm 2007-10-28 made SML/NJ happy;
2007-10-28 wenzelm 2007-10-28 safe_exit: controlled_execution;
2007-10-27 obua 2007-10-27 better compute oracle
2007-10-27 obua 2007-10-27 better compute oracle
2007-10-27 obua 2007-10-27 adapted Compute...
2007-10-27 krauss 2007-10-27 use "fun" for definition of "member" -> authentic syntax
2007-10-27 haftmann 2007-10-27 ASCIIfied README
2007-10-27 haftmann 2007-10-27 added list comprehension syntax
2007-10-26 wenzelm 2007-10-26 locale_const: in_class workaround prevents additional locale version of class consts;
2007-10-26 wenzelm 2007-10-26 notation: associate syntax to checked-unchecked term;
2007-10-26 wenzelm 2007-10-26 export class_prefix; removed obsolete const hiding;