isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

substantial improvement in codegen iml
2006-03-07, by haftmann
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
2006-03-07, by mengj
relevance_filter takes input axioms as Term.term.
2006-03-07, by mengj
Proof reconstruction now only takes names of theorems as input.
2006-03-07, by mengj
Added tptp_write_file to write all necessary ATP input clauses to one file.
2006-03-07, by mengj
tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
2006-03-07, by mengj
Added functions to retrieve local and global atpset rules.
2006-03-07, by mengj
Moved the settings for ATP time limit to res_atp.ML
2006-03-07, by mengj
Merged res_atp_setup.ML into res_atp.ML.
2006-03-07, by mengj
When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
2006-03-07, by mengj
Merged res_atp_setup.ML into res_atp.ML.
2006-03-07, by mengj
SELECT_GOAL: fixed trivial case;
2006-03-05, by wenzelm
fixed a typo in a comment
2006-03-05, by webertj
tuned;
2006-03-04, by wenzelm
method: SelectGoals;
2006-03-04, by wenzelm
method: syntax for SelectGoals;
2006-03-04, by wenzelm
text: added SelectGoals;
2006-03-04, by wenzelm
tuned conj_curry;
2006-03-04, by wenzelm
added extract, retrofit;
2006-03-04, by wenzelm
added mk_conjunction;
2006-03-04, by wenzelm
method: restriction to first n sub-goals;
2006-03-04, by wenzelm
minor changes
2006-03-03, by nipkow
more examples
2006-03-03, by nipkow
changed and retracted change of location of code lemmas.
2006-03-03, by nipkow
ignore repeated vars on lhs, cleanup
2006-03-03, by nipkow
improvements for nbe
2006-03-03, by haftmann
reformatting
2006-03-02, by paulson
subset_refl now included using the atp attribute
2006-03-02, by paulson
moved the "use" directive
2006-03-02, by paulson
fixed the bugs itroduced by the previous commit
2006-03-02, by urbanc
made some small changes to generate nicer latex-output
2006-03-02, by urbanc
split the files
2006-03-02, by urbanc
Added in a signature.
2006-03-02, by mengj
fixed a problem where a permutation is not analysed
2006-03-01, by urbanc
streamlined the proof
2006-03-01, by urbanc
refined representation of codegen intermediate language
2006-03-01, by haftmann
some small tunings
2006-03-01, by urbanc
added fresh_fun_eqvt theorem to the theorem collection
2006-03-01, by urbanc
added initialisation-code for finite_guess
2006-03-01, by urbanc
made some small tunings in the decision-procedure
2006-03-01, by urbanc
Added setup for "atpset" (a rule set for ATPs).
2006-03-01, by mengj
Added file Tools/res_atpset.ML.
2006-03-01, by mengj
Merged HOL and FOL clauses and combined some functions.
2006-03-01, by mengj
A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
2006-03-01, by mengj
some minor tuning on the proofs
2006-03-01, by urbanc
initial commit (especially 2nd half needs to be cleaned up)
2006-02-28, by urbanc
removal of theory blacklist
2006-02-28, by paulson
new order for arity clauses
2006-02-28, by paulson
fixed but in freeze_spec
2006-02-28, by paulson
splitting up METAHYPS into smaller functions
2006-02-28, by paulson
typos
2006-02-28, by paulson
added a finite_guess tactic, which solves
2006-02-27, by urbanc
class package and codegen refinements
2006-02-27, by haftmann
added nbe
2006-02-27, by haftmann
added temp. nbe test
2006-02-27, by nipkow
added nbe, updated neb_*
2006-02-27, by nipkow
added nbe
2006-02-27, by nipkow
Typo.
2006-02-27, by ballarin
added support for arbitrary atoms in the simproc
2006-02-27, by urbanc
put_thms: do_index;
2006-02-26, by wenzelm
rewrite_goals_rule_aux: actually use prems if present;
2006-02-26, by wenzelm
add_local: do_index;
2006-02-26, by wenzelm
replaced the lemma at_two by at_different;
2006-02-26, by urbanc
improved the decision-procedure for permutations;
2006-02-26, by urbanc
improved codegen bootstrap
2006-02-25, by haftmann
change in codegen syntax
2006-02-25, by haftmann
some refinements
2006-02-25, by haftmann
added more detailed data to consts
2006-02-25, by haftmann
Reverted to old interface of AxClass.add_inst_arity(_i)
2006-02-24, by berghofe
Adapted to Florian's recent changes to the AxClass package.
2006-02-24, by berghofe
added lemmas
2006-02-23, by urbanc
make SML/NJ happy;
2006-02-23, by wenzelm
Default type level is T_FULL now.
2006-02-23, by mengj
eprover removes tmp files too.
2006-02-23, by mengj
vampire/eprover methods can now be applied repeatedly until they fail.
2006-02-23, by mengj
removed obsolete meta_conjunction_tr';
2006-02-22, by wenzelm
rew: handle conjunctionI/D1/D2;
2006-02-22, by wenzelm
simplified Pure conjunction, based on actual const;
2006-02-22, by wenzelm
removed rename_indexes_wrt;
2006-02-22, by wenzelm
renamed class_axms to class_intros;
2006-02-22, by wenzelm
tuned proofs;
2006-02-22, by wenzelm
simplified Pure conjunction;
2006-02-22, by wenzelm
not_equal: replaced syntax translation by abbreviation;
2006-02-22, by wenzelm
abandoned merge_alists' in favour of generic AList.merge
2006-02-22, by haftmann
added Tools/nbe, fixes
2006-02-21, by nipkow
added Tools/nbe
2006-02-21, by nipkow
New normalization-by-evaluation package
2006-02-21, by nipkow
distinct (op =);
2006-02-21, by wenzelm
fixed
2006-02-20, by kleing
Inclusion of subset_refl in ATP calls
2006-02-20, by paulson
Fix variable-naming bug (?) by removing a needless recursive call
2006-02-20, by paulson
slight code generator serialization improvements
2006-02-20, by haftmann
moved intro_classes from AxClass to ClassPackage
2006-02-20, by haftmann
fixed document
2006-02-19, by kleing
* denumerability of rationals by Benjamin Porter, based on NatPair (by Stefan Richter)
2006-02-19, by kleing
added a few lemmas to do with permutation-equivalence for the
2006-02-19, by urbanc
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
2006-02-19, by kleing
use minimal imports
2006-02-19, by huffman
use qualified name for return
2006-02-19, by huffman
dest_def: tuned error msg;
2006-02-18, by wenzelm
const constraints: provide TFrees instead of TVars,
2006-02-17, by wenzelm
checkpoint/copy_node: reset body context;
2006-02-17, by wenzelm
global_qeds: transfer body context;
2006-02-17, by wenzelm
add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
2006-02-17, by wenzelm
constrain: assert const declaration, optional type (i.e. may delete constraints);
2006-02-17, by wenzelm
removed Import/lazy_scan.ML;
2006-02-17, by wenzelm
hyperlinks in the PDF work now
2006-02-17, by paulson
replaced Symbol.explode by explode
2006-02-17, by obua
updated mailing list archive link
2006-02-17, by haftmann
use monomorphic sequences / scanners
2006-02-17, by obua
make maybe into a real type constructor; remove monad syntax
2006-02-17, by huffman
use VectorScannerSeq instead of ListScannerSeq in xml.ML
2006-02-16, by obua
removed lazy_scan
2006-02-16, by obua
improved scanning
2006-02-16, by obua
tuned;
2006-02-16, by wenzelm
Abstract Natural Numbers with polymorphic recursion.
2006-02-16, by wenzelm
new-style definitions/abbreviations;
2006-02-16, by wenzelm
added ex/Abstract_NAT.thy;
2006-02-16, by wenzelm
tuned;
2006-02-16, by wenzelm
tuned;
2006-02-16, by wenzelm