Mercurial
Mercurial
>
repos
>
testboard
/ 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.
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
notation: associate syntax to checkedunchecked term;
20071026, by wenzelm
export class_prefix;
20071026, by wenzelm
tuned
20071026, by haftmann
changed order of class parameters
20071026, by haftmann
dropped square syntax
20071026, by haftmann
localized monotonicity; tuned syntax
20071026, by haftmann
dropped "brown" syntax
20071026, by haftmann
replaced Secure.evaluate by ML_Context.evaluate;
20071026, by wenzelm
asm_rewrite_goal_tac: avoiding PRIMITIVE lets informative exceptions (from simprocs) get through;
20071026, by wenzelm
proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;
20071026, by wenzelm
print the defined constants when finished; tuned
20071026, by krauss
adjusted
20071026, by haftmann
tuned
20071026, by haftmann
added NEWS entry for function package
20071026, by krauss
added hint for algebra
20071026, by haftmann
less
more

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