Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-56
+56
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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
continued localization
2007-10-30, by haftmann
fixed typo
2007-10-29, by haftmann
added nbe
2007-10-29, by haftmann
test_proof: do not change Proofterm.proofs here (not thread-safe);
2007-10-29, by wenzelm
improved notion of 'nicer' fact names (observe some name space properties);
2007-10-29, by wenzelm
export is_hidden;
2007-10-29, by wenzelm
added bool_ord;
2007-10-29, by wenzelm
qualified Proofterm.proofs;
2007-10-29, by wenzelm
fun/function: generate case names for induction rules
2007-10-29, by krauss
append/member: more light-weight way to declare authentic syntax;
2007-10-28, by wenzelm
made SML/NJ happy;
2007-10-28, by wenzelm
safe_exit: controlled_execution;
2007-10-28, by wenzelm
better compute oracle
2007-10-27, by obua
better compute oracle
2007-10-27, by obua
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-56
+56
+100
+300
+1000
+3000
+10000
+30000
tip