2007-11-06 haftmann 2007-11-06 removed subclass edge ordered_ring < lordered_ring
2007-11-06 haftmann 2007-11-06 renamed lordered_*_* to lordered_*_add_*; further localization
2007-11-05 wenzelm 2007-11-05 tuned satisfy_thm;
2007-11-05 wenzelm 2007-11-05 removed unused compose_hhf, comp_hhf;
2007-11-05 obua 2007-11-05 corrected fucked up integer tuning
2007-11-05 kleing 2007-11-05 misc lemmas about prefix, postfix, and parallel
2007-11-05 kleing 2007-11-05 add root.bib for Word document
2007-11-05 kleing 2007-11-05 move itself into HOL types
2007-11-05 kleing 2007-11-05 rev_nth
2007-11-05 kleing 2007-11-05 tranclD2 (tranclD at the other end) + trancl_power
2007-11-05 kleing 2007-11-05 acknowledge authors
2007-11-05 kleing 2007-11-05 cite Jeremy's avocs article
2007-11-05 wenzelm 2007-11-05 simplified LocalTheory.reinit; tuned;
2007-11-05 wenzelm 2007-11-05 misc cleanup of init functions; renamed init_cmd to context; simplified LocalTheory.reinit;
2007-11-05 wenzelm 2007-11-05 TheoryTarget.context;
2007-11-05 wenzelm 2007-11-05 simplified LocalTheory.reinit;
2007-11-05 wenzelm 2007-11-05 improved error message for missing predicates;
2007-11-05 nipkow 2007-11-05 added lemmas
2007-11-05 ballarin 2007-11-05 Use of export rather than standard in interpretation.
2007-11-05 ballarin 2007-11-05 Removed inst_morphism'; satisfy_thm avoids compose.
2007-11-05 ballarin 2007-11-05 Interpretation with named equations.
2007-11-05 ballarin 2007-11-05 Type instance of thm mk_left_commute in locales.
2007-11-05 ballarin 2007-11-05 Tests enforce proper export behaviour.
2007-11-05 nipkow 2007-11-05 removed advanced recdef section and replaced it by citation of Alex's tutorial.
2007-11-05 nipkow 2007-11-05 fix
2007-11-05 obua 2007-11-05 no Gencode.ML
2007-11-05 krauss 2007-11-05 changed "treemap" example to "mirror"
2007-11-05 nipkow 2007-11-05 added lemmas
2007-11-04 wenzelm 2007-11-04 replaced cc/ld phase by PolyML.SaveState.saveState (potentially more efficient);
2007-11-04 wenzelm 2007-11-04 removed obsolete ProofGeneral/parsing.ML;
2007-11-04 wenzelm 2007-11-04 activated new script parser;
2007-11-04 wenzelm 2007-11-04 Output.add_mode default prevents escapes from ProofGeneral mode;
2007-11-04 wenzelm 2007-11-04 added ProofGeneral/pgml_isabelle.ML;
2007-11-04 wenzelm 2007-11-04 the all-important ML antiquotations are back; tuned;
2007-11-02 haftmann 2007-11-02 generic tactic Method.intros_tac
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.