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