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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
the allimportant ML antiquotations are back;
20071104, by wenzelm
generic tactic Method.intros_tac
20071102, by haftmann
clarified theory target interface
20071102, by haftmann
more precise treatment of prove_subclass
20071102, by haftmann
proper reinitialisation after subclass
20071102, by haftmann
clarified
20071102, by haftmann
tweaked
20071102, by paulson
recdef to fun
20071102, by paulson
*** empty log message ***
20071102, by nipkow
Added reference to Jeremy Dawson's paper on the word library.
20071102, by kleing
recdef > fun
20071102, by nipkow
added Fun
20071102, by nipkow
tuned
20071102, by haftmann
recdef > fun
20071101, by nipkow
*** empty log message ***
20071101, by nipkow
Catch exceptions arising during the abstraction operation.
20071031, by paulson
Added example for the ideal membership problem solved by algebra
20071031, by chaieb
Added field ideal into entry  uses by algebra method to prove the ideal membership problem
20071031, by chaieb
changed signature according to normalizer_data.ML
20071031, by chaieb
tuned
20071031, by chaieb
(1) signatures updated according to normalizer_data.ML (added field ideal in entry);
20071031, 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)
20071031, by chaieb
exported field_comp_conv: a numerical conversion over fields
20071031, by chaieb
dropped AxClass
20071031, by haftmann
tuned
20071031, by haftmann
Handle Subscript exception when looking up bound variables.
20071030, by berghofe
Added wellformedness check to Abst case in function prf_of.
20071030, by berghofe
added omission
20071030, by haftmann
bugfixes concerning strange theorems
20071030, by paulson
fixed typo
20071030, by haftmann
const antiquotation clarified
20071030, by haftmann
clarified
20071030, by haftmann
handling of notation in class target
20071030, by haftmann
fixed document preparation
20071030, by haftmann
improved website integration
20071030, by haftmann
adjusted
20071030, by haftmann
split library index into templates
20071030, by haftmann
split library index into templates
20071030, by haftmann
structured
20071030, by haftmann
tidied version
20071030, by haftmann
simplified proof
20071030, by haftmann
continued localization
20071030, by haftmann
fixed typo
20071029, by haftmann
added nbe
20071029, by haftmann
test_proof: do not change Proofterm.proofs here (not threadsafe);
20071029, by wenzelm
improved notion of 'nicer' fact names (observe some name space properties);
20071029, by wenzelm
export is_hidden;
20071029, by wenzelm
added bool_ord;
20071029, by wenzelm
qualified Proofterm.proofs;
20071029, by wenzelm
fun/function: generate case names for induction rules
20071029, by krauss
append/member: more lightweight way to declare authentic syntax;
20071028, by wenzelm
made SML/NJ happy;
20071028, by wenzelm
safe_exit: controlled_execution;
20071028, by wenzelm
better compute oracle
20071027, by obua
better compute oracle
20071027, by obua
adapted Compute...
20071027, by obua
use "fun" for definition of "member" > authentic syntax
20071027, by krauss
ASCIIfied README
20071027, by haftmann
added list comprehension syntax
20071027, by haftmann
locale_const: in_class workaround prevents additional locale version of class consts;
20071026, by wenzelm
less
more

(0)
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip