Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-96
+96
+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.
-- 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
changed the HOL_basic_ss back and selectively added
2005-11-13, by urbanc
exchanged HOL_ss for HOL_basic_ss in the simplification
2005-11-13, by urbanc
a proof step corrected due to the changement in the presburger method.
2005-11-11, by chaieb
old argument "abs" is replaced by "no_abs". Abstraction is turned on by default.
2005-11-11, by chaieb
add header
2005-11-11, by huffman
tuned proofs;
2005-11-10, by wenzelm
moved find_free to term.ML;
2005-11-10, by wenzelm
guess: Seq.hd;
2005-11-10, by wenzelm
guess: Toplevel.proof;
2005-11-10, by wenzelm
added find_free (from Isar/proof_context.ML);
2005-11-10, by wenzelm
curried multiply;
2005-11-10, by wenzelm
induct method: fixes;
2005-11-10, by wenzelm
uncurried Consts.typargs;
2005-11-10, by wenzelm
renamed Thm.cgoal_of to Thm.cprem_of;
2005-11-10, by wenzelm
duplicate axioms in ATP linkup, and general fixes
2005-11-10, by paulson
tidying
2005-11-10, by paulson
called the induction principle "unsafe" instead of "test".
2005-11-10, by urbanc
Skolemization by inference, but not quite finished
2005-11-09, by paulson
Explicit data structures for some Isar language elements.
2005-11-09, by wenzelm
tuned;
2005-11-09, by wenzelm
tvars_intr_list: natural argument order;
2005-11-09, by wenzelm
moved datatype elem to element.ML;
2005-11-09, by wenzelm
P.context_element, P.locale_element;
2005-11-09, by wenzelm
Element.context;
2005-11-09, by wenzelm
use existing exeption Empty;
2005-11-09, by wenzelm
avoid code redundancy;
2005-11-09, by wenzelm
tuned comments;
2005-11-09, by wenzelm
removed obsolete term set operations;
2005-11-09, by wenzelm
P.locale_element;
2005-11-09, by wenzelm
added fold_terms;
2005-11-09, by wenzelm
added Isar/element.ML;
2005-11-09, by wenzelm
Thm.varifyT': natural argument order;
2005-11-09, by wenzelm
added join function
2005-11-09, by haftmann
allowing indentation of 'theory' keyword
2005-11-08, by haftmann
simplified after_qed;
2005-11-08, by wenzelm
avoid prove_plain, export_plain, simplified after_qed;
2005-11-08, by wenzelm
removed export_plain;
2005-11-08, by wenzelm
renamed assert_prop to ensure_prop;
2005-11-08, by wenzelm
renamed goals.ML to old_goals.ML;
2005-11-08, by wenzelm
export compose_hhf;
2005-11-08, by wenzelm
removed impose_hyps, satisfy_hyps;
2005-11-08, by wenzelm
const args: do not store variable names (unused);
2005-11-08, by wenzelm
renamed goals.ML to old_goals.ML;
2005-11-08, by wenzelm
(fix for accidental commit)
2005-11-08, by haftmann
(codegen)
2005-11-08, by haftmann
generate pattern combinators for new datatypes
2005-11-08, by huffman
reimplemented Case syntax using print/parse translations; moved as-patterns to separate section
2005-11-07, by huffman
add case syntax for type one
2005-11-07, by huffman
remove syntax for as-patterns
2005-11-07, by huffman
avoid 'as' as identifier;
2005-11-07, by wenzelm
avoid 'as' as identifier;
2005-11-07, by wenzelm
Added strong induction theorem (currently only axiomatized!).
2005-11-07, by berghofe
Initial commit.
2005-11-07, by urbanc
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-96
+96
+100
+300
+1000
+3000
+10000
+30000
tip