Mercurial
Mercurial
>
repos
>
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
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.
Implemented proof of weak induction theorem.
2005-10-28, by berghofe
Added "deepen" method.
2005-10-28, by berghofe
circumvented smlnj value restriction
2005-10-28, by haftmann
added extraction interface for code generator
2005-10-28, by haftmann
Added (optional) arguments to the tactics
2005-10-28, by urbanc
cleaned up nth, nth_update, nth_map and nth_string functions
2005-10-28, by haftmann
Removed legacy prove_goalw_cterm command.
2005-10-28, by berghofe
got rid of obsolete prove_goalw_cterm
2005-10-28, by paulson
swapped add_datatype result
2005-10-28, by haftmann
removed obfuscating PStrStrTab
2005-10-28, by haftmann
reachable - abandoned foldl_map in favor of fold_map
2005-10-28, by haftmann
Added Tools/res_hol_clause.ML
2005-10-28, by mengj
Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
2005-10-28, by mengj
Added "writeln_strs" to the signature
2005-10-28, by mengj
Added several new functions that are used to prove HOL goals. Added new methods "vampireH" and "eproverH" that can prove both FOL and HOL goals. The old "vampire" and "eprover" methods are renamed to "vampireF" and "eproverF"; they can only prove FOL goals.
2005-10-28, by mengj
Added new functions to handle HOL goals and lemmas.
2005-10-28, by mengj
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
2005-10-28, by mengj
Added several functions to the signature.
2005-10-28, by mengj
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
2005-10-28, by mengj
sorted lemma lists
2005-10-27, by paulson
* HOL: alternative iff syntax;
2005-10-27, by wenzelm
consts: monomorphic;
2005-10-27, by wenzelm
removed inappropriate monomorphic test;
2005-10-27, by wenzelm
replaced Defs.monomorphic by Sign.monomorphic;
2005-10-27, by wenzelm
alternative iff syntax for equality on booleans, with print_mode 'iff';
2005-10-27, by wenzelm
added module Pure/General/rat.ML
2005-10-27, by haftmann
tidied away duplicate thm
2005-10-26, by paulson
EVERY;
2005-10-25, by wenzelm
traceIt: plain term;
2005-10-25, by wenzelm
val legacy = ref false;
2005-10-25, by wenzelm
prove_raw: cterms, explicit asms;
2005-10-25, by wenzelm
avoid legacy goals;
2005-10-25, by wenzelm
legacy = ref true for the time being -- avoid volumious warnings;
2005-10-22, by wenzelm
tuned;
2005-10-21, by wenzelm
avoid OldGoals shortcuts;
2005-10-21, by wenzelm
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
2005-10-21, by wenzelm
Internal goals.
2005-10-21, by wenzelm
renamed triv_goal to goalI, rev_triv_goal to goalD;
2005-10-21, by wenzelm
tuned header;
2005-10-21, by wenzelm
Goal.norm_hhf_rule;
2005-10-21, by wenzelm
export add_binds_i;
2005-10-21, by wenzelm
load_file: setmp OldGoals.legacy true;
2005-10-21, by wenzelm
improved check_result;
2005-10-21, by wenzelm
Goal.prove_plain;
2005-10-21, by wenzelm
do not export find_thms;
2005-10-21, by wenzelm
use obsolete goals.ML here;
2005-10-21, by wenzelm
Goal.conclude;
2005-10-21, by wenzelm
moved SELECT_GOAL to goal.ML;
2005-10-21, by wenzelm
moved norm_hhf_rule, prove etc. to goal.ML;
2005-10-21, by wenzelm
added simplification tactics and rules (from meta_simplifier.ML);
2005-10-21, by wenzelm
moved various simplification tactics and rules to simplifier.ML;
2005-10-21, by wenzelm
warn_obsolete for goal commands -- danger of disrupting a local proof context;
2005-10-21, by wenzelm
renamed triv_goal to goalI, rev_triv_goal to goalD;
2005-10-21, by wenzelm
added goal.ML;
2005-10-21, by wenzelm
added goal.ML;
2005-10-21, by wenzelm
Goal.norm_hhf_rule, Goal.init;
2005-10-21, by wenzelm
avoid triv_goal and home-grown meta_allE;
2005-10-21, by wenzelm
OldGoals;
2005-10-21, by wenzelm
proper header;
2005-10-21, by wenzelm
avoid home-grown meta_allE;
2005-10-21, by wenzelm
Goal.prove;
2005-10-21, by wenzelm
avoid shortcuts from OldGoals;
2005-10-21, by wenzelm
added simplified settings for Poly/ML 4.x (commented out);
2005-10-21, by wenzelm
reverted (accidental?) change of 1.148;
2005-10-21, by wenzelm
abandoned rational number functions in favor of General/rat.ML
2005-10-21, by haftmann
introduced functions from Pure/General/rat.ML
2005-10-21, by haftmann
slight corrections
2005-10-21, by haftmann
substantially improved integration of website into distribution framework
2005-10-21, by haftmann
substantially improved integration of website into distribution framework
2005-10-21, by haftmann
substantially improved integration of website into distribution framework
2005-10-21, by haftmann
substantially improved integration of website into distribution framework
2005-10-21, by haftmann
towards an improved website/makedist integration
2005-10-21, by haftmann
towards an improved website/makedist integration
2005-10-21, by haftmann
added default distinfo.mak
2005-10-21, by haftmann
towards an improved website/makedist integration
2005-10-21, by haftmann
towards an improved website/makedist integration
2005-10-21, by haftmann
added rounding functions
2005-10-21, by haftmann
Merged theory ResAtpOracle.thy into ResAtpMethods.thy
2005-10-21, by mengj
obsolete;
2005-10-19, by wenzelm
removed add_inductive_x;
2005-10-19, by wenzelm
removed obsolete add_datatype_x;
2005-10-19, by wenzelm
removed obsolete thy_syntax.ML;
2005-10-19, by wenzelm
removed obsolete old_symbol_source;
2005-10-19, by wenzelm
removed obsolete non-Isar theory format and old Isar theory headers;
2005-10-19, by wenzelm
removed old-style theory format;
2005-10-19, by wenzelm
avoid lagacy read function;
2005-10-19, by wenzelm
added thm(s) retrieval functions (from goals.ML);
2005-10-19, by wenzelm
removed obsolete old-locales;
2005-10-19, by wenzelm
removed obsolete axclass_tac, add_inst_subclass_x, add_inst_arity_x;
2005-10-19, by wenzelm
removed obsolete Thy/thy_parse.ML, Thy/thy_scan.ML, Thy/thy_syn.ML;
2005-10-19, by wenzelm
removed obsolete old-style syntax;
2005-10-19, by wenzelm
removed obsolete IOA/meta_theory/ioa_package.ML;
2005-10-19, by wenzelm
removed obsolete domain/interface.ML, IOA/meta_theory/ioa_package.ML;
2005-10-19, by wenzelm
removed obsolete domain/interface.ML;
2005-10-19, by wenzelm
removed obsolete add_typedef_x;
2005-10-19, by wenzelm
removed print_exn (better let the toplevel do this);
2005-10-19, by wenzelm
removed obsolete add_recdef_old;
2005-10-19, by wenzelm
removed obsolete HOL/thy_syntax.ML;
2005-10-19, by wenzelm
* Theory syntax: discontinued non-Isar format and old Isar headers;
2005-10-19, by wenzelm
replaced commafy by existing commas;
2005-10-19, by wenzelm
updated;
2005-10-19, by wenzelm
isatool fixheaders;
2005-10-19, by wenzelm
fix headers;
2005-10-19, by wenzelm
added table functor instance for pairs of strings
2005-10-19, by haftmann
added subgraph
2005-10-19, by haftmann
added join
2005-10-19, by haftmann
slight improvements for website
2005-10-19, by haftmann
moved VAMPIRE_HOME, E_HOME to section "External reasoning tools" -- commented out by default!
2005-10-19, by wenzelm
More functions are added to the signature of ResClause
2005-10-19, by mengj
*** empty log message ***
2005-10-19, by mengj
added 2 lemmas
2005-10-19, by nipkow
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
2005-10-19, by mengj
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
2005-10-18, by wenzelm
tuned error msg;
2005-10-18, by wenzelm
renamed atomize_rule to atomize_cterm;
2005-10-18, by wenzelm
ObjectLogic.atomize_cterm;
2005-10-18, by wenzelm
use simplified Toplevel.proof etc.;
2005-10-18, by wenzelm
back: Toplevel.actual/skip_proof;
2005-10-18, by wenzelm
renamed set_context to context;
2005-10-18, by wenzelm
renamed set_context to context;
2005-10-18, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-120
+120
+1000
+3000
+10000
+30000
tip