2007-11-06 haftmann 2007-11-06 Class.init now similiar to Locale.init
2007-11-06 haftmann 2007-11-06 CRITICAL force
2007-11-06 haftmann 2007-11-06 autoquickcheck message
2007-11-06 haftmann 2007-11-06 added explicit signature
2007-11-06 haftmann 2007-11-06 simplified specification of *_abs class
2007-11-06 wenzelm 2007-11-06 tuned;
2007-11-06 haftmann 2007-11-06 added autoquickcheck
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