isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

TheoryTarget.context;
2007-11-05, by wenzelm
simplified LocalTheory.reinit;
2007-11-05, by wenzelm
improved error message for missing predicates;
2007-11-05, by wenzelm
added lemmas
2007-11-05, by nipkow
Use of export rather than standard in interpretation.
2007-11-05, by ballarin
Removed inst_morphism'; satisfy_thm avoids compose.
2007-11-05, by ballarin
Interpretation with named equations.
2007-11-05, by ballarin
Type instance of thm mk_left_commute in locales.
2007-11-05, by ballarin
Tests enforce proper export behaviour.
2007-11-05, by ballarin
removed advanced recdef section and replaced it by citation of Alex's tutorial.
2007-11-05, by nipkow
fix
2007-11-05, by nipkow
no Gencode.ML
2007-11-05, by obua
changed "treemap" example to "mirror"
2007-11-05, by krauss
added lemmas
2007-11-05, by nipkow
replaced cc/ld phase by PolyML.SaveState.saveState (potentially more efficient);
2007-11-04, by wenzelm
removed obsolete ProofGeneral/parsing.ML;
2007-11-04, by wenzelm
activated new script parser;
2007-11-04, by wenzelm
Output.add_mode default prevents escapes from ProofGeneral mode;
2007-11-04, by wenzelm
added ProofGeneral/pgml_isabelle.ML;
2007-11-04, by wenzelm
the all-important ML antiquotations are back;
2007-11-04, by wenzelm
generic tactic Method.intros_tac
2007-11-02, by haftmann
clarified theory target interface
2007-11-02, by haftmann
more precise treatment of prove_subclass
2007-11-02, by haftmann
proper reinitialisation after subclass
2007-11-02, by haftmann
clarified
2007-11-02, by haftmann
tweaked
2007-11-02, by paulson
recdef to fun
2007-11-02, by paulson
*** empty log message ***
2007-11-02, by nipkow
Added reference to Jeremy Dawson's paper on the word library.
2007-11-02, by kleing
recdef -> fun
2007-11-02, by nipkow
added Fun
2007-11-02, by nipkow
tuned
2007-11-02, by haftmann
recdef -> fun
2007-11-01, by nipkow
*** empty log message ***
2007-11-01, by nipkow
Catch exceptions arising during the abstraction operation.
2007-10-31, by paulson
Added example for the ideal membership problem solved by algebra
2007-10-31, by chaieb
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
2007-10-31, by chaieb
changed signature according to normalizer_data.ML
2007-10-31, by chaieb
tuned
2007-10-31, by chaieb
(1) signatures updated according to normalizer_data.ML (added field ideal in entry);
2007-10-31, by chaieb
(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, by chaieb
exported field_comp_conv: a numerical conversion over fields
2007-10-31, by chaieb
dropped AxClass
2007-10-31, by haftmann
tuned
2007-10-31, by haftmann
Handle Subscript exception when looking up bound variables.
2007-10-30, by berghofe
Added well-formedness check to Abst case in function prf_of.
2007-10-30, by berghofe
added omission
2007-10-30, by haftmann
bugfixes concerning strange theorems
2007-10-30, by paulson
fixed typo
2007-10-30, by haftmann
const antiquotation clarified
2007-10-30, by haftmann
clarified
2007-10-30, by haftmann
handling of notation in class target
2007-10-30, by haftmann
fixed document preparation
2007-10-30, by haftmann
improved website integration
2007-10-30, by haftmann
adjusted
2007-10-30, by haftmann
split library index into templates
2007-10-30, by haftmann
split library index into templates
2007-10-30, by haftmann
structured
2007-10-30, by haftmann
tidied version
2007-10-30, by haftmann
simplified proof
2007-10-30, by haftmann

less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle