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 JavaScript-enabled browsers.
new treatment of polymorphic types, using Sign.const_typargs
2005-11-22, by paulson
added codegen package
2005-11-21, by haftmann
added serializer
2005-11-21, by haftmann
tweak
2005-11-21, by paulson
fixed some inconveniencies in website
2005-11-21, by haftmann
CONJUNCTS;
2005-11-19, by wenzelm
tuned;
2005-11-19, by wenzelm
Goal.norm_hhf_protected;
2005-11-19, by wenzelm
added coinduct attribute;
2005-11-19, by wenzelm
added CONJUNCTS: treat conjunction as separate sub-goals;
2005-11-19, by wenzelm
simpset: added reorient field, set_reorient;
2005-11-19, by wenzelm
tuned norm_hhf_protected;
2005-11-19, by wenzelm
removed conj_mono;
2005-11-19, by wenzelm
induct: CONJUNCTS for multiple goals;
2005-11-19, by wenzelm
tuned induct syntax;
2005-11-19, by wenzelm
FOL: -p 2;
2005-11-19, by wenzelm
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
2005-11-18, by chaieb
-- changed the interface of functions vampire_oracle and eprover_oracle.
2005-11-18, by mengj
-- terms are fully typed.
2005-11-18, by mengj
-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.
2005-11-18, by mengj
-- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
2005-11-18, by mengj
-- added combinator reduction axioms (typed and untyped) for HOL goals.
2005-11-18, by mengj
-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).
2005-11-18, by mengj
-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.
2005-11-18, by mengj
-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
2005-11-18, by mengj
tuned document;
2005-11-16, by wenzelm
tuned;
2005-11-16, by wenzelm
improved induction proof: local defs/fixes;
2005-11-16, by wenzelm
tuned Pattern.match/unify;
2005-11-16, by wenzelm
added deskolem;
2005-11-16, by wenzelm
added THEN_ALL_NEW_CASES;
2005-11-16, by wenzelm
added revert_skolem, mk_def, add_def;
2005-11-16, by wenzelm
ProofContext.mk_def;
2005-11-16, by wenzelm
Term.betapplys;
2005-11-16, by wenzelm
tuned Pattern.match/unify;
2005-11-16, by wenzelm
added betapplys;
2005-11-16, by wenzelm
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
2005-11-16, by wenzelm
tuned;
2005-11-16, by wenzelm
norm_hhf: no normalization of protected props;
2005-11-16, by wenzelm
added protect_cong, cong_mono_thm;
2005-11-16, by wenzelm
induct: support local definitions to be passed through the induction;
2005-11-16, by wenzelm
Trueprop: use ObjectLogic.judgment etc.;
2005-11-16, by wenzelm
Term.betapply;
2005-11-16, by wenzelm
new version of "tryres" allowing multiple unifiers (apparently needed for
2005-11-16, by paulson
pgmlsymbolson: append Symbol.xsymbolsN at end!
2005-11-16, by wenzelm
better no -d option;
2005-11-15, by wenzelm
added generic transformators
2005-11-15, by haftmann
removal of is_hol
2005-11-14, by paulson
added module system
2005-11-14, by haftmann
added modules for code generator generation two, not operational yet
2005-11-14, by haftmann
class_package - operational view on type classes
2005-11-14, by haftmann
string_of_alist - convenient q'n'd printout function
2005-11-14, by haftmann
support for polyml-4.2.0;
2005-11-14, by wenzelm
new syntax for class_package
2005-11-14, by haftmann
added const_instance;
2005-11-14, by wenzelm
added instance;
2005-11-14, by wenzelm
added ML-Systems/polyml-4.1.4-patch.ML, ML-Systems/polyml-4.2.0.ML;
2005-11-14, by wenzelm
Compatibility wrapper for Poly/ML 4.2.0.
2005-11-14, by wenzelm
tuned;
2005-11-14, by wenzelm
added a few equivariance lemmas (they need to be automated
2005-11-14, by urbanc
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip