| Mon, 31 Oct 2005 16:00:15 +0100 |
haftmann |
fold_index replacing foldln
|
changeset |
files
|
| Mon, 31 Oct 2005 01:43:22 +0100 |
nipkow |
A few new lemmas
|
changeset |
files
|
| Sun, 30 Oct 2005 10:55:56 +0100 |
urbanc |
tuned my last commit
|
changeset |
files
|
| Sun, 30 Oct 2005 10:37:57 +0100 |
urbanc |
simplified the abs_supp_approx proof and tuned some comments in
|
changeset |
files
|
| Sat, 29 Oct 2005 15:01:25 +0200 |
urbanc |
Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
|
changeset |
files
|
| Sat, 29 Oct 2005 14:37:32 +0200 |
urbanc |
1) have adjusted the swapping of the result type
|
changeset |
files
|
| Fri, 28 Oct 2005 22:37:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:32:55 +0200 |
wenzelm |
lthms_containing: not o valid_thms;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:15 +0200 |
wenzelm |
added fact_tac, some_fact_tac;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:13 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:12 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:11 +0200 |
wenzelm |
added fact method;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:09 +0200 |
wenzelm |
tuned ProofContext.export interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:07 +0200 |
wenzelm |
syntax for literal facts;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:06 +0200 |
wenzelm |
removed try_dest_Goal, use Logic.unprotect;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:04 +0200 |
wenzelm |
added cgoal_of;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:03 +0200 |
wenzelm |
accomodate simplified Thm.lift_rule;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:02 +0200 |
wenzelm |
export cong_modifiers, simp_modifiers';
|
changeset |
files
|
| Fri, 28 Oct 2005 22:28:00 +0200 |
wenzelm |
certify_term: tuned monomorphic consts;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:59 +0200 |
wenzelm |
datatype thmref: added Fact;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:58 +0200 |
wenzelm |
Logic.lift_all;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:57 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:56 +0200 |
wenzelm |
renamed Goal.norm_hhf_rule to Goal.norm_hhf;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:55 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:54 +0200 |
wenzelm |
added add_local/add_global;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:52 +0200 |
wenzelm |
added incr_indexes;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:51 +0200 |
wenzelm |
renamed Goal constant to prop;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:47 +0200 |
wenzelm |
accomodate simplified Thm.lift_rule;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:46 +0200 |
wenzelm |
Logic.unprotect;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:44 +0200 |
wenzelm |
literal facts;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:27:41 +0200 |
wenzelm |
* Pure/Isar: literal facts;
|
changeset |
files
|
| Fri, 28 Oct 2005 22:26:10 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 28 Oct 2005 20:18:37 +0200 |
webertj |
unnecessary imports removed
|
changeset |
files
|
| Fri, 28 Oct 2005 18:53:26 +0200 |
urbanc |
fixed case names in the weak induction principle and
|
changeset |
files
|
| Fri, 28 Oct 2005 18:22:26 +0200 |
berghofe |
Implemented proof of weak induction theorem.
|
changeset |
files
|
| Fri, 28 Oct 2005 17:59:07 +0200 |
berghofe |
Added "deepen" method.
|
changeset |
files
|
| Fri, 28 Oct 2005 17:27:49 +0200 |
haftmann |
circumvented smlnj value restriction
|
changeset |
files
|
| Fri, 28 Oct 2005 17:27:04 +0200 |
haftmann |
added extraction interface for code generator
|
changeset |
files
|
| Fri, 28 Oct 2005 16:43:46 +0200 |
urbanc |
Added (optional) arguments to the tactics
|
changeset |
files
|
| Fri, 28 Oct 2005 16:35:40 +0200 |
haftmann |
cleaned up nth, nth_update, nth_map and nth_string functions
|
changeset |
files
|
| Fri, 28 Oct 2005 13:52:57 +0200 |
berghofe |
Removed legacy prove_goalw_cterm command.
|
changeset |
files
|
| Fri, 28 Oct 2005 12:22:34 +0200 |
paulson |
got rid of obsolete prove_goalw_cterm
|
changeset |
files
|
| Fri, 28 Oct 2005 09:36:19 +0200 |
haftmann |
swapped add_datatype result
|
changeset |
files
|
| Fri, 28 Oct 2005 09:35:04 +0200 |
haftmann |
removed obfuscating PStrStrTab
|
changeset |
files
|
| Fri, 28 Oct 2005 08:40:55 +0200 |
haftmann |
reachable - abandoned foldl_map in favor of fold_map
|
changeset |
files
|
| Fri, 28 Oct 2005 02:30:53 +0200 |
mengj |
Added Tools/res_hol_clause.ML
|
changeset |
files
|
| Fri, 28 Oct 2005 02:30:12 +0200 |
mengj |
Added a new file res_hol_clause.ML to Reconstruction.thy. This file is used to translate HOL formulae into FOL clauses.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:29:01 +0200 |
mengj |
Added "writeln_strs" to the signature
|
changeset |
files
|
| Fri, 28 Oct 2005 02:28:20 +0200 |
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.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:27:19 +0200 |
mengj |
Added new functions to handle HOL goals and lemmas.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:25:57 +0200 |
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.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:24:58 +0200 |
mengj |
Added several functions to the signature.
|
changeset |
files
|
| Fri, 28 Oct 2005 02:23:49 +0200 |
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.
|
changeset |
files
|
| Thu, 27 Oct 2005 18:25:33 +0200 |
paulson |
sorted lemma lists
|
changeset |
files
|
| Thu, 27 Oct 2005 13:59:06 +0200 |
wenzelm |
* HOL: alternative iff syntax;
|
changeset |
files
|
| Thu, 27 Oct 2005 13:54:43 +0200 |
wenzelm |
consts: monomorphic;
|
changeset |
files
|
| Thu, 27 Oct 2005 13:54:42 +0200 |
wenzelm |
removed inappropriate monomorphic test;
|
changeset |
files
|
| Thu, 27 Oct 2005 13:54:40 +0200 |
wenzelm |
replaced Defs.monomorphic by Sign.monomorphic;
|
changeset |
files
|
| Thu, 27 Oct 2005 13:54:38 +0200 |
wenzelm |
alternative iff syntax for equality on booleans, with print_mode 'iff';
|
changeset |
files
|
| Thu, 27 Oct 2005 08:14:05 +0200 |
haftmann |
added module Pure/General/rat.ML
|
changeset |
files
|
| Wed, 26 Oct 2005 16:31:53 +0200 |
paulson |
tidied away duplicate thm
|
changeset |
files
|
| Tue, 25 Oct 2005 18:38:21 +0200 |
wenzelm |
EVERY;
|
changeset |
files
|
| Tue, 25 Oct 2005 18:18:59 +0200 |
wenzelm |
traceIt: plain term;
|
changeset |
files
|
| Tue, 25 Oct 2005 18:18:58 +0200 |
wenzelm |
val legacy = ref false;
|
changeset |
files
|
| Tue, 25 Oct 2005 18:18:57 +0200 |
wenzelm |
prove_raw: cterms, explicit asms;
|
changeset |
files
|
| Tue, 25 Oct 2005 18:18:49 +0200 |
wenzelm |
avoid legacy goals;
|
changeset |
files
|
| Sat, 22 Oct 2005 01:22:10 +0200 |
wenzelm |
legacy = ref true for the time being -- avoid volumious warnings;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:20:29 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:17:00 +0200 |
wenzelm |
avoid OldGoals shortcuts;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:16:57 +0200 |
wenzelm |
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
|
changeset |
files
|
| Fri, 21 Oct 2005 18:15:00 +0200 |
wenzelm |
Internal goals.
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:59 +0200 |
wenzelm |
renamed triv_goal to goalI, rev_triv_goal to goalD;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:58 +0200 |
wenzelm |
tuned header;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:57 +0200 |
wenzelm |
Goal.norm_hhf_rule;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:56 +0200 |
wenzelm |
export add_binds_i;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:55 +0200 |
wenzelm |
load_file: setmp OldGoals.legacy true;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:54 +0200 |
wenzelm |
improved check_result;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:53 +0200 |
wenzelm |
Goal.prove_plain;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:52 +0200 |
wenzelm |
do not export find_thms;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:51 +0200 |
wenzelm |
use obsolete goals.ML here;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:50 +0200 |
wenzelm |
Goal.conclude;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:49 +0200 |
wenzelm |
moved SELECT_GOAL to goal.ML;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:48 +0200 |
wenzelm |
moved norm_hhf_rule, prove etc. to goal.ML;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:47 +0200 |
wenzelm |
added simplification tactics and rules (from meta_simplifier.ML);
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:46 +0200 |
wenzelm |
moved various simplification tactics and rules to simplifier.ML;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:45 +0200 |
wenzelm |
warn_obsolete for goal commands -- danger of disrupting a local proof context;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:44 +0200 |
wenzelm |
renamed triv_goal to goalI, rev_triv_goal to goalD;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:43 +0200 |
wenzelm |
added goal.ML;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:42 +0200 |
wenzelm |
added goal.ML;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:41 +0200 |
wenzelm |
Goal.norm_hhf_rule, Goal.init;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:40 +0200 |
wenzelm |
avoid triv_goal and home-grown meta_allE;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:38 +0200 |
wenzelm |
OldGoals;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:37 +0200 |
wenzelm |
proper header;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:36 +0200 |
wenzelm |
avoid home-grown meta_allE;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:34 +0200 |
wenzelm |
Goal.prove;
|
changeset |
files
|
| Fri, 21 Oct 2005 18:14:32 +0200 |
wenzelm |
avoid shortcuts from OldGoals;
|
changeset |
files
|
| Fri, 21 Oct 2005 16:34:22 +0200 |
wenzelm |
added simplified settings for Poly/ML 4.x (commented out);
|
changeset |
files
|
| Fri, 21 Oct 2005 16:22:59 +0200 |
wenzelm |
reverted (accidental?) change of 1.148;
|
changeset |
files
|
| Fri, 21 Oct 2005 14:49:49 +0200 |
haftmann |
abandoned rational number functions in favor of General/rat.ML
|
changeset |
files
|
| Fri, 21 Oct 2005 14:49:04 +0200 |
haftmann |
introduced functions from Pure/General/rat.ML
|
changeset |
files
|
| Fri, 21 Oct 2005 14:47:37 +0200 |
haftmann |
slight corrections
|
changeset |
files
|
| Fri, 21 Oct 2005 10:32:59 +0200 |
haftmann |
substantially improved integration of website into distribution framework
|
changeset |
files
|
| Fri, 21 Oct 2005 10:32:04 +0200 |
haftmann |
substantially improved integration of website into distribution framework
|
changeset |
files
|
| Fri, 21 Oct 2005 10:27:02 +0200 |
haftmann |
substantially improved integration of website into distribution framework
|
changeset |
files
|
| Fri, 21 Oct 2005 10:21:38 +0200 |
haftmann |
substantially improved integration of website into distribution framework
|
changeset |
files
|
| Fri, 21 Oct 2005 09:54:03 +0200 |
haftmann |
towards an improved website/makedist integration
|
changeset |
files
|
| Fri, 21 Oct 2005 09:18:27 +0200 |
haftmann |
towards an improved website/makedist integration
|
changeset |
files
|
| Fri, 21 Oct 2005 09:08:42 +0200 |
haftmann |
added default distinfo.mak
|
changeset |
files
|
| Fri, 21 Oct 2005 09:05:52 +0200 |
haftmann |
towards an improved website/makedist integration
|
changeset |
files
|
| Fri, 21 Oct 2005 09:05:52 +0200 |
haftmann |
towards an improved website/makedist integration
|
changeset |
files
|
| Fri, 21 Oct 2005 08:23:45 +0200 |
haftmann |
added rounding functions
|
changeset |
files
|
| Fri, 21 Oct 2005 02:57:22 +0200 |
mengj |
Merged theory ResAtpOracle.thy into ResAtpMethods.thy
|
changeset |
files
|
| Wed, 19 Oct 2005 21:53:34 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:50 +0200 |
wenzelm |
removed add_inductive_x;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:49 +0200 |
wenzelm |
removed obsolete add_datatype_x;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:48 +0200 |
wenzelm |
removed obsolete thy_syntax.ML;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:47 +0200 |
wenzelm |
removed obsolete old_symbol_source;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:46 +0200 |
wenzelm |
removed obsolete non-Isar theory format and old Isar theory headers;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:45 +0200 |
wenzelm |
removed old-style theory format;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:44 +0200 |
wenzelm |
avoid lagacy read function;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:43 +0200 |
wenzelm |
added thm(s) retrieval functions (from goals.ML);
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:42 +0200 |
wenzelm |
removed obsolete old-locales;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:41 +0200 |
wenzelm |
removed obsolete axclass_tac, add_inst_subclass_x, add_inst_arity_x;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:40 +0200 |
wenzelm |
removed obsolete Thy/thy_parse.ML, Thy/thy_scan.ML, Thy/thy_syn.ML;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:38 +0200 |
wenzelm |
removed obsolete old-style syntax;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:37 +0200 |
wenzelm |
removed obsolete IOA/meta_theory/ioa_package.ML;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:36 +0200 |
wenzelm |
removed obsolete domain/interface.ML, IOA/meta_theory/ioa_package.ML;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:35 +0200 |
wenzelm |
removed obsolete domain/interface.ML;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:34 +0200 |
wenzelm |
removed obsolete add_typedef_x;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:33 +0200 |
wenzelm |
removed print_exn (better let the toplevel do this);
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:32 +0200 |
wenzelm |
removed obsolete add_recdef_old;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:31 +0200 |
wenzelm |
removed obsolete HOL/thy_syntax.ML;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:30 +0200 |
wenzelm |
* Theory syntax: discontinued non-Isar format and old Isar headers;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:29 +0200 |
wenzelm |
replaced commafy by existing commas;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:28 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:27 +0200 |
wenzelm |
isatool fixheaders;
|
changeset |
files
|
| Wed, 19 Oct 2005 21:52:07 +0200 |
wenzelm |
fix headers;
|
changeset |
files
|
| Wed, 19 Oct 2005 17:21:53 +0200 |
haftmann |
added table functor instance for pairs of strings
|
changeset |
files
|
| Wed, 19 Oct 2005 17:19:52 +0200 |
haftmann |
added subgraph
|
changeset |
files
|
| Wed, 19 Oct 2005 17:19:37 +0200 |
haftmann |
added join
|
changeset |
files
|
| Wed, 19 Oct 2005 16:32:09 +0200 |
haftmann |
slight improvements for website
|
changeset |
files
|
| Wed, 19 Oct 2005 14:51:12 +0200 |
wenzelm |
moved VAMPIRE_HOME, E_HOME to section "External reasoning tools" -- commented out by default!
|
changeset |
files
|
| Wed, 19 Oct 2005 13:59:33 +0200 |
mengj |
More functions are added to the signature of ResClause
|
changeset |
files
|
| Wed, 19 Oct 2005 10:25:46 +0200 |
mengj |
*** empty log message ***
|
changeset |
files
|
| Wed, 19 Oct 2005 06:46:45 +0200 |
nipkow |
added 2 lemmas
|
changeset |
files
|
| Wed, 19 Oct 2005 06:33:24 +0200 |
mengj |
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:37 +0200 |
wenzelm |
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:36 +0200 |
wenzelm |
tuned error msg;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:35 +0200 |
wenzelm |
renamed atomize_rule to atomize_cterm;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:34 +0200 |
wenzelm |
ObjectLogic.atomize_cterm;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:33 +0200 |
wenzelm |
use simplified Toplevel.proof etc.;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:32 +0200 |
wenzelm |
back: Toplevel.actual/skip_proof;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:31 +0200 |
wenzelm |
renamed set_context to context;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:30 +0200 |
wenzelm |
renamed set_context to context;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:29 +0200 |
wenzelm |
functor: no Simplifier argument;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:28 +0200 |
wenzelm |
moved helper lemma to HilbertChoice.thy;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:27 +0200 |
wenzelm |
Simplifier.theory_context;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:26 +0200 |
wenzelm |
added lemma exE_some (from specification_package.ML);
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:25 +0200 |
wenzelm |
Simplifier.theory_context;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:24 +0200 |
wenzelm |
tuned error msg;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:23 +0200 |
wenzelm |
Simplifier.context/theory_context;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:22 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 18 Oct 2005 15:08:38 +0200 |
paulson |
new interface to make_conjecture_clauses
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:25 +0200 |
wenzelm |
* Simplifier: simpset of a running simplification process contains a proof context;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:24 +0200 |
wenzelm |
added type_solver (uses Simplifier.the_context);
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:23 +0200 |
wenzelm |
added pos/negDivAlg_induct declarations (from Main.thy);
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:22 +0200 |
wenzelm |
moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:21 +0200 |
wenzelm |
removed obsolete/experimental context components (superceded by Simplifier.the_context);
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:20 +0200 |
wenzelm |
added set/addloop' for simpset dependent loopers;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:19 +0200 |
wenzelm |
functor: no Simplifier argument;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:18 +0200 |
wenzelm |
change_claset(_of): more abtract interface;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:17 +0200 |
wenzelm |
functor: no Simplifier argument;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:16 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:15 +0200 |
wenzelm |
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:13 +0200 |
wenzelm |
change_claset/simpset;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:10 +0200 |
wenzelm |
change_claset/simpset;
|
changeset |
files
|
| Mon, 17 Oct 2005 19:19:29 +0200 |
berghofe |
Improved proof of injectivity theorems to make it work on
|
changeset |
files
|
| Mon, 17 Oct 2005 18:34:51 +0200 |
berghofe |
Fixed bug in proof of support theorem (it failed on constructors with no arguments).
|
changeset |
files
|
| Mon, 17 Oct 2005 17:42:24 +0200 |
berghofe |
Implemented proofs for support and freshness theorems.
|
changeset |
files
|
| Mon, 17 Oct 2005 17:40:34 +0200 |
urbanc |
deleted leading space in the definition of fresh
|
changeset |
files
|
| Mon, 17 Oct 2005 12:30:57 +0200 |
berghofe |
Initial revision.
|
changeset |
files
|
| Sat, 15 Oct 2005 00:14:30 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:09:20 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:09:07 +0200 |
wenzelm |
added ML_type, ML_struct;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:15 +0200 |
wenzelm |
more;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:14 +0200 |
wenzelm |
* antiquotations ML_type, ML_struct;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:13 +0200 |
wenzelm |
added guess;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:12 +0200 |
wenzelm |
added antiquotations ML_type, ML_struct;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:11 +0200 |
wenzelm |
use perl for test/stat;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:10 +0200 |
wenzelm |
export strip_params;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:09 +0200 |
wenzelm |
note_thmss, read/cert_vars etc.: natural argument order;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:08 +0200 |
wenzelm |
goal statements: before_qed argument;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:07 +0200 |
wenzelm |
added 'guess', which derives the obtained context from the course of reasoning;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:06 +0200 |
wenzelm |
added primitive_text, succeed_text;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:05 +0200 |
wenzelm |
goal statements: accomodate before_qed argument;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:04 +0200 |
wenzelm |
goal statements: accomodate before_qed argument;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:03 +0200 |
wenzelm |
added 'guess';
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:01 +0200 |
wenzelm |
added no_facts;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:00 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:07:59 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Fri, 14 Oct 2005 15:34:56 +0200 |
paulson |
signature changes
|
changeset |
files
|
| Fri, 14 Oct 2005 14:36:39 +0200 |
haftmann |
added module rat.ML for rational numbers
|
changeset |
files
|
| Fri, 14 Oct 2005 13:04:38 +0200 |
isatest |
longer time out for test (kleing)
|
changeset |
files
|
| Fri, 14 Oct 2005 11:36:14 +0200 |
paulson |
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
|
changeset |
files
|
| Fri, 14 Oct 2005 10:19:50 +0200 |
paulson |
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
|
changeset |
files
|
| Thu, 13 Oct 2005 11:58:22 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Wed, 12 Oct 2005 18:17:48 +0200 |
webertj |
counter added to SAT signature
|
changeset |
files
|
| Wed, 12 Oct 2005 17:06:22 +0200 |
webertj |
no proof reconstruction when quick_and_dirty is set
|
changeset |
files
|
| Wed, 12 Oct 2005 10:49:07 +0200 |
paulson |
tidying
|
changeset |
files
|
| Wed, 12 Oct 2005 03:02:18 +0200 |
huffman |
domain package generates compactness lemmas for new constructors
|
changeset |
files
|
| Wed, 12 Oct 2005 03:01:30 +0200 |
huffman |
add ML bindings for compactness lemmas
|
changeset |
files
|
| Wed, 12 Oct 2005 03:01:09 +0200 |
huffman |
added compactness theorems
|
changeset |
files
|
| Wed, 12 Oct 2005 01:43:37 +0200 |
huffman |
added compactness lemmas; cleaned up
|
changeset |
files
|
| Tue, 11 Oct 2005 23:47:29 +0200 |
huffman |
added compactness theorems in locale iso
|
changeset |
files
|
| Tue, 11 Oct 2005 23:27:49 +0200 |
huffman |
added several theorems in locale iso
|
changeset |
files
|
| Tue, 11 Oct 2005 23:27:14 +0200 |
huffman |
added xsymbols syntax for pairs; cleaned up
|
changeset |
files
|
| Tue, 11 Oct 2005 23:23:39 +0200 |
huffman |
added theorem typedef_compact
|
changeset |
files
|
| Tue, 11 Oct 2005 23:22:12 +0200 |
huffman |
rearranged subsections; added theorems expand_cfun_eq, expand_cfun_less
|
changeset |
files
|
| Tue, 11 Oct 2005 23:19:50 +0200 |
huffman |
cleaned up; renamed less_fun to expand_fun_less
|
changeset |
files
|
| Tue, 11 Oct 2005 17:30:00 +0200 |
nipkow |
added hd lemma
|
changeset |
files
|
| Tue, 11 Oct 2005 15:04:11 +0200 |
paulson |
simplifying the treatment of clausification
|
changeset |
files
|
| Tue, 11 Oct 2005 15:03:36 +0200 |
paulson |
simplifying the treatment of nameless theorems
|
changeset |
files
|
| Tue, 11 Oct 2005 14:02:33 +0200 |
wenzelm |
expand: error on undefined/empty env variable;
|
changeset |
files
|
| Tue, 11 Oct 2005 14:02:32 +0200 |
wenzelm |
added assert;
|
changeset |
files
|
| Tue, 11 Oct 2005 13:30:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:08 +0200 |
wenzelm |
added string_of_pid;
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:07 +0200 |
wenzelm |
raw symbols: allow non-ASCII chars (e.g. UTF-8);
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:06 +0200 |
wenzelm |
moved string_of_pid to ML-Systems;
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:05 +0200 |
wenzelm |
ML_SUFFIX in targets (experimental);
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:04 +0200 |
wenzelm |
cleanup backup images;
|
changeset |
files
|
| Mon, 10 Oct 2005 15:35:29 +0200 |
paulson |
small tidy-up of utility functions
|
changeset |
files
|
| Mon, 10 Oct 2005 14:43:45 +0200 |
wenzelm |
updated print_tac;
|
changeset |
files
|
| Mon, 10 Oct 2005 05:46:17 +0200 |
huffman |
add names to infix declarations
|
changeset |
files
|
| Mon, 10 Oct 2005 05:30:02 +0200 |
huffman |
new syntax translations for continuous lambda abstraction
|
changeset |
files
|
| Mon, 10 Oct 2005 04:38:26 +0200 |
huffman |
removed Istrictify; simplified some proofs
|
changeset |
files
|
| Mon, 10 Oct 2005 04:12:31 +0200 |
huffman |
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
|
changeset |
files
|
| Mon, 10 Oct 2005 04:03:09 +0200 |
huffman |
cleaned up
|
changeset |
files
|
| Mon, 10 Oct 2005 04:00:40 +0200 |
huffman |
added theorem typedef_chfin
|
changeset |
files
|
| Mon, 10 Oct 2005 03:55:39 +0200 |
huffman |
replaced foldr' with foldr1
|
changeset |
files
|
| Mon, 10 Oct 2005 03:47:00 +0200 |
huffman |
cleaned up; renamed "Porder.op <<" to "Porder.<<"
|
changeset |
files
|
| Sun, 09 Oct 2005 17:06:03 +0200 |
webertj |
Tactics sat and satx reimplemented, several improvements
|
changeset |
files
|
| Sat, 08 Oct 2005 23:43:15 +0200 |
wenzelm |
tuned Memory.hilim;
|
changeset |
files
|
| Sat, 08 Oct 2005 23:43:14 +0200 |
wenzelm |
get rid of feeder -- at the cost of batch-only commit-at-exit;
|
changeset |
files
|
| Sat, 08 Oct 2005 23:36:01 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Sat, 08 Oct 2005 23:05:59 +0200 |
wenzelm |
-nort option;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:42 +0200 |
wenzelm |
added could_unify;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:41 +0200 |
wenzelm |
more efficient check_specified, much less invocations;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:40 +0200 |
wenzelm |
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:39 +0200 |
wenzelm |
uses susp.ML, lazy_seq.ML, lazy_scan.ML;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:38 +0200 |
wenzelm |
added Import/susp.ML, Import/lazy_seq.ML, Import/lasy_scan.ML;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:38 +0200 |
wenzelm |
minor tweaks for Poplog/PML;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:37 +0200 |
wenzelm |
tuned memory limits;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:36 +0200 |
wenzelm |
Int.max;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:35 +0200 |
wenzelm |
minor tweaks for Poplog/PML;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:34 +0200 |
wenzelm |
minor tweaks for Poplog/PML;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:33 +0200 |
wenzelm |
initial pop11 code for ML use/use_string;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:32 +0200 |
wenzelm |
Poplog/PML: ML_SUFFIX=.psv;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:31 +0200 |
wenzelm |
support ML_SUFFIX;
|
changeset |
files
|
| Sat, 08 Oct 2005 18:51:03 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sat, 08 Oct 2005 15:20:58 +0200 |
nipkow |
fix due to new neq_simproc
|
changeset |
files
|
| Fri, 07 Oct 2005 23:29:00 +0200 |
wenzelm |
removed obsolete comment;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:26 +0200 |
wenzelm |
added idtypdummy_ast_tr;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:25 +0200 |
wenzelm |
added syntax for _idtdummy, _idtypdummy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:24 +0200 |
wenzelm |
added absdummy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:23 +0200 |
wenzelm |
removed obsolete dummy_pat_tr;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:22 +0200 |
wenzelm |
Term.absdummy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:21 +0200 |
wenzelm |
removed obsolete ex/Tuple.thy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:19 +0200 |
wenzelm |
replaced _K by dummy abstraction;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:18 +0200 |
wenzelm |
print_translation: does not handle _idtdummy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:15 +0200 |
wenzelm |
added dummy variable binding;
|
changeset |
files
|
| Fri, 07 Oct 2005 20:41:10 +0200 |
nipkow |
changes due to new neq_simproc in simpdata.ML
|
changeset |
files
|
| Fri, 07 Oct 2005 18:49:20 +0200 |
wenzelm |
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
|
changeset |
files
|
| Fri, 07 Oct 2005 18:49:19 +0200 |
wenzelm |
Term.str_of_term;
|
changeset |
files
|
| Fri, 07 Oct 2005 17:57:21 +0200 |
paulson |
minor code tidyig
|
changeset |
files
|
| Fri, 07 Oct 2005 15:08:28 +0200 |
paulson |
code restructuring
|
changeset |
files
|
| Fri, 07 Oct 2005 11:29:24 +0200 |
paulson |
more tidying. Fixed process management bugs and race condition
|
changeset |
files
|
| Thu, 06 Oct 2005 10:14:22 +0200 |
paulson |
major simplification: removal of the goalstring argument
|
changeset |
files
|
| Thu, 06 Oct 2005 10:13:34 +0200 |
berghofe |
Optimized getPreds and getSuccs.
|
changeset |
files
|
| Thu, 06 Oct 2005 08:58:58 +0200 |
haftmann |
adjusted sydney to new website
|
changeset |
files
|
| Thu, 06 Oct 2005 08:56:15 +0200 |
haftmann |
changed sydney share
|
changeset |
files
|
| Wed, 05 Oct 2005 19:28:12 +0200 |
wenzelm |
added Poplog/PML version 15.6/2.1 (experimental!);
|
changeset |
files
|
| Wed, 05 Oct 2005 18:38:43 +0200 |
haftmann |
added fold_nodes, map_node_yield
|
changeset |
files
|
| Wed, 05 Oct 2005 18:38:28 +0200 |
haftmann |
added merge, tuned
|
changeset |
files
|
| Wed, 05 Oct 2005 14:01:32 +0200 |
nipkow |
added last in set lemma
|
changeset |
files
|
| Wed, 05 Oct 2005 11:18:06 +0200 |
paulson |
improved process handling. tidied
|
changeset |
files
|
| Wed, 05 Oct 2005 10:56:06 +0200 |
paulson |
more signals
|
changeset |
files
|
| Tue, 04 Oct 2005 23:39:42 +0200 |
nipkow |
new hd/rev/last lemmas
|
changeset |
files
|
| Tue, 04 Oct 2005 23:30:46 +0200 |
nipkow |
new lemmas
|
changeset |
files
|
| Tue, 04 Oct 2005 21:39:16 +0200 |
wenzelm |
added compiler and runtime options;
|
changeset |
files
|
| Tue, 04 Oct 2005 21:33:09 +0200 |
wenzelm |
Poplog/PML startup script.
|
changeset |
files
|
| Tue, 04 Oct 2005 20:38:13 +0200 |
wenzelm |
Compatibility file for Poplog/PML (version 15.6/2.1).
|
changeset |
files
|
| Tue, 04 Oct 2005 19:05:37 +0200 |
wenzelm |
Substring.all = Substring.full;
|
changeset |
files
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
changeset |
files
|
| Tue, 04 Oct 2005 16:47:40 +0200 |
wenzelm |
find_theorems: support * wildcard in name: criterion;
|
changeset |
files
|
| Tue, 04 Oct 2005 16:47:39 +0200 |
wenzelm |
* Command 'find_theorems': support * wildcard in name: criterion.
|
changeset |
files
|
| Tue, 04 Oct 2005 16:05:08 +0200 |
wenzelm |
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
|
changeset |
files
|
| Tue, 04 Oct 2005 14:58:44 +0200 |
haftmann |
added redirect.html
|
changeset |
files
|
| Tue, 04 Oct 2005 14:37:06 +0200 |
haftmann |
better error handling
|
changeset |
files
|
| Tue, 04 Oct 2005 11:15:09 +0200 |
haftmann |
improved linktest
|
changeset |
files
|
| Tue, 04 Oct 2005 10:58:46 +0200 |
haftmann |
removed removed IntFloor
|
changeset |
files
|
| Tue, 04 Oct 2005 10:55:14 +0200 |
haftmann |
fixed broken link
|
changeset |
files
|
| Tue, 04 Oct 2005 10:52:43 +0200 |
haftmann |
fixed broken mailto: link
|
changeset |
files
|
| Tue, 04 Oct 2005 09:59:01 +0200 |
paulson |
fixed the ascii-armouring of goalstring
|
changeset |
files
|
| Tue, 04 Oct 2005 09:58:38 +0200 |
paulson |
reset clause counter
|
changeset |
files
|
| Tue, 04 Oct 2005 09:58:17 +0200 |
paulson |
theorems need names
|
changeset |
files
|
| Tue, 04 Oct 2005 09:19:17 +0200 |
haftmann |
support for setting local permissions
|
changeset |
files
|
| Tue, 04 Oct 2005 08:49:24 +0200 |
haftmann |
improved dependency build
|
changeset |
files
|
| Tue, 04 Oct 2005 08:14:15 +0200 |
haftmann |
added conf/ to .cvsignore
|
changeset |
files
|
| Fri, 30 Sep 2005 18:18:34 +0200 |
aspinall |
Add icon for interface.
Isabelle2005
|
changeset |
files
|
| Fri, 30 Sep 2005 17:54:04 +0200 |
aspinall |
Move welcomemsg and helpdoc to pgip_isar.xml
|
changeset |
files
|
| Fri, 30 Sep 2005 17:52:18 +0200 |
aspinall |
Add helpdocs and welcomemsg here instead of hard wiring in proof_general.ML.
|
changeset |
files
|
| Fri, 30 Sep 2005 17:33:22 +0200 |
aspinall |
Explanatory text
|
changeset |
files
|
| Fri, 30 Sep 2005 17:28:04 +0200 |
aspinall |
Schema files (for information, and validating pgip_isar.xml)
|
changeset |
files
|
| Fri, 30 Sep 2005 17:24:51 +0200 |
aspinall |
Schema for PGIP
|
changeset |
files
|
| Fri, 30 Sep 2005 15:28:43 +0200 |
wenzelm |
pruned notes about Poly/ML;
|
changeset |
files
|
| Fri, 30 Sep 2005 15:17:04 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Fri, 30 Sep 2005 13:47:36 +0200 |
aspinall |
Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
|
changeset |
files
|
| Fri, 30 Sep 2005 11:43:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 30 Sep 2005 10:58:11 +0200 |
aspinall |
Fix for guiconfig -> displayconfig element rename
|
changeset |
files
|
| Fri, 30 Sep 2005 09:52:46 +0200 |
paulson |
theorems need names
|
changeset |
files
|
| Thu, 29 Sep 2005 19:37:20 +0200 |
wenzelm |
refer to $PRG instead of (old) rsync-isabelle;
|
changeset |
files
|
| Thu, 29 Sep 2005 18:01:12 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 29 Sep 2005 17:09:11 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 29 Sep 2005 17:08:52 +0200 |
wenzelm |
pdfsetup.sty: better not rely on ifpdf.sty;
|
changeset |
files
|
| Thu, 29 Sep 2005 17:02:57 +0200 |
paulson |
simprules need names
|
changeset |
files
|
| Thu, 29 Sep 2005 15:50:46 +0200 |
wenzelm |
export debug_bounds;
|
changeset |
files
|
| Thu, 29 Sep 2005 15:50:45 +0200 |
wenzelm |
explicit dependencies of SAT vs. Refute;
|
changeset |
files
|
| Thu, 29 Sep 2005 15:50:44 +0200 |
wenzelm |
explicit dependencies of SAT vs. Refute;
|
changeset |
files
|
| Thu, 29 Sep 2005 15:50:43 +0200 |
wenzelm |
Isabelle2005 (October 2005);
|
changeset |
files
|
| Thu, 29 Sep 2005 15:31:34 +0200 |
nipkow |
Added a few lemmas
|
changeset |
files
|
| Thu, 29 Sep 2005 12:45:16 +0200 |
paulson |
reduction in tracing files
|
changeset |
files
|
| Thu, 29 Sep 2005 12:45:04 +0200 |
paulson |
improvements for problem generation
|
changeset |
files
|
| Thu, 29 Sep 2005 12:44:25 +0200 |
paulson |
moved concat_with_and to watcher.ML
|
changeset |
files
|
| Thu, 29 Sep 2005 12:43:40 +0200 |
paulson |
a name for empty_not_insert
|
changeset |
files
|
| Thu, 29 Sep 2005 12:33:26 +0200 |
berghofe |
Simplifier now removes flex-flex constraints from theorem returned by prover.
|
changeset |
files
|
| Thu, 29 Sep 2005 12:30:30 +0200 |
berghofe |
Optimized and exported flexflex_unique.
|
changeset |
files
|
| Thu, 29 Sep 2005 01:12:16 +0200 |
wenzelm |
make signature constraint actually work;
|
changeset |
files
|
| Thu, 29 Sep 2005 01:09:39 +0200 |
wenzelm |
activate signature constraints;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:59:03 +0200 |
wenzelm |
HOL4 image is back;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:59:02 +0200 |
wenzelm |
tuned default operation: use internal modify;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:59:01 +0200 |
wenzelm |
abstract_rule: tuned exception msgs;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:59:00 +0200 |
wenzelm |
back to simple 'defs' (cf. revision 1.79 of theory.ML);
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:59 +0200 |
wenzelm |
back to simple 'defs' (cf. revision 1.79);
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:58 +0200 |
wenzelm |
removed revert_bound;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:57 +0200 |
wenzelm |
print_theory: discontinued final consts;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:56 +0200 |
wenzelm |
Theory.add_finals_i;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:55 +0200 |
wenzelm |
more finalconsts;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:54 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 28 Sep 2005 18:50:42 +0200 |
webertj |
pointer to HOL/ex/SAT_Examples.thy added
|
changeset |
files
|
| Wed, 28 Sep 2005 16:58:06 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 28 Sep 2005 15:13:02 +0200 |
wenzelm |
more reliable check for PDF output using ifpdf.sty;
|
changeset |
files
|
| Wed, 28 Sep 2005 14:41:43 +0200 |
webertj |
pre_sat_tac moved towards end of file
|
changeset |
files
|
| Wed, 28 Sep 2005 14:16:34 +0200 |
haftmann |
adjusted www links
|
changeset |
files
|
| Wed, 28 Sep 2005 14:16:12 +0200 |
webertj |
comment fixed
|
changeset |
files
|
| Wed, 28 Sep 2005 13:17:23 +0200 |
obua |
mapped "-->" to "hol4-->"
|
changeset |
files
|
| Wed, 28 Sep 2005 11:50:15 +0200 |
wenzelm |
avoid naming existing tags in explanations;
|
changeset |
files
|
| Wed, 28 Sep 2005 11:50:14 +0200 |
wenzelm |
revert 'defs' advertisement;
|
changeset |
files
|
| Wed, 28 Sep 2005 11:50:13 +0200 |
wenzelm |
revert 'defs' advertisement;
|
changeset |
files
|
| Wed, 28 Sep 2005 11:16:27 +0200 |
paulson |
time limit option; fixed bug concerning first line of ATP output
|
changeset |
files
|
| Wed, 28 Sep 2005 11:15:33 +0200 |
paulson |
streamlined theory; conformance to recent publication
|
changeset |
files
|
| Wed, 28 Sep 2005 11:14:26 +0200 |
paulson |
new lemma
|
changeset |
files
|
| Wed, 28 Sep 2005 09:14:44 +0200 |
haftmann |
better appearance in lynx and netscape4
|
changeset |
files
|
| Wed, 28 Sep 2005 08:57:19 +0200 |
haftmann |
MB instead of KB
|
changeset |
files
|
| Tue, 27 Sep 2005 20:43:39 +0200 |
wenzelm |
renamed packages to download;
|
changeset |
files
|
| Tue, 27 Sep 2005 17:24:27 +0200 |
wenzelm |
more details about incomplete 'defs';
|
changeset |
files
|
| Tue, 27 Sep 2005 17:14:27 +0200 |
wenzelm |
renamed "Packages" to "Download";
|
changeset |
files
|
| Tue, 27 Sep 2005 17:13:11 +0200 |
haftmann |
build bed
|
changeset |
files
|
| Tue, 27 Sep 2005 17:09:46 +0200 |
haftmann |
build bed
|
changeset |
files
|
| Tue, 27 Sep 2005 17:09:46 +0200 |
haftmann |
build bed
|
changeset |
files
|
| Tue, 27 Sep 2005 17:03:54 +0200 |
haftmann |
slight corrections
|
changeset |
files
|
| Tue, 27 Sep 2005 17:01:49 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 27 Sep 2005 17:01:10 +0200 |
wenzelm |
renamed "Packages" to "Download";
|
changeset |
files
|
| Tue, 27 Sep 2005 16:52:38 +0200 |
haftmann |
fixed dead link
|
changeset |
files
|
| Tue, 27 Sep 2005 16:52:38 +0200 |
haftmann |
fixed dead link
|
changeset |
files
|
| Tue, 27 Sep 2005 16:52:24 +0200 |
haftmann |
improved linkcheck
|
changeset |
files
|
| Tue, 27 Sep 2005 16:33:36 +0200 |
haftmann |
added simple linktester for isabelle website
|
changeset |
files
|
| Tue, 27 Sep 2005 16:28:11 +0200 |
wenzelm |
warn about Poly/ML segfault problem;
|
changeset |
files
|
| Tue, 27 Sep 2005 15:30:37 +0200 |
haftmann |
website preparation for Isabelle2005
|
changeset |
files
|
| Tue, 27 Sep 2005 14:41:41 +0200 |
obua |
corrected spelling bug
|
changeset |
files
|
| Tue, 27 Sep 2005 14:39:35 +0200 |
obua |
added defs disclaimer
|
changeset |
files
|
| Tue, 27 Sep 2005 12:16:06 +0200 |
berghofe |
nat_number_of is no longer declared as code lemma, since this turned
|
changeset |
files
|
| Tue, 27 Sep 2005 12:14:39 +0200 |
berghofe |
Inserted clause for nat in number_of_codegen again ("code unfold" turned
|
changeset |
files
|
| Tue, 27 Sep 2005 12:13:17 +0200 |
berghofe |
Optimized unfold_attr.
|
changeset |
files
|
| Tue, 27 Sep 2005 11:39:27 +0200 |
wenzelm |
removed link to HOL4, which is not in the library right now;
|
changeset |
files
|
| Tue, 27 Sep 2005 11:27:07 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 27 Sep 2005 11:03:38 +0200 |
berghofe |
Added entries for code_module, code_library, and value.
|
changeset |
files
|
| Tue, 27 Sep 2005 11:02:16 +0200 |
berghofe |
Tuned.
|
changeset |
files
|
| Mon, 26 Sep 2005 20:52:36 +0200 |
wenzelm |
updates for Isabelle2005;
|
changeset |
files
|
| Mon, 26 Sep 2005 20:51:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 26 Sep 2005 20:12:51 +0200 |
berghofe |
Updated description of code generator.
|
changeset |
files
|
| Mon, 26 Sep 2005 19:19:15 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Mon, 26 Sep 2005 19:19:14 +0200 |
wenzelm |
moved disambiguate_frees to ProofKernel;
|
changeset |
files
|
| Mon, 26 Sep 2005 19:19:13 +0200 |
wenzelm |
quote 'value';
|
changeset |
files
|
| Mon, 26 Sep 2005 19:19:12 +0200 |
wenzelm |
yet another atempt to get doc/Contents right;
|
changeset |
files
|
| Mon, 26 Sep 2005 19:04:31 +0200 |
berghofe |
Renamed wf_rec to wfrec in consts_code declaration.
|
changeset |
files
|
| Mon, 26 Sep 2005 17:14:48 +0200 |
wenzelm |
really copy doc/Contents;
|
changeset |
files
|
| Mon, 26 Sep 2005 16:10:19 +0200 |
obua |
Release HOL4 and HOLLight Importer.
|
changeset |
files
|
| Mon, 26 Sep 2005 15:56:28 +0200 |
wenzelm |
copy doc/Contents;
|
changeset |
files
|
| Mon, 26 Sep 2005 15:17:33 +0200 |
skalberg |
Made sure all lemmas now have names (especially so that certain of them
|
changeset |
files
|
| Mon, 26 Sep 2005 13:12:24 +0200 |
wenzelm |
echo HOL_USERDIR_OPTIONS;
|
changeset |
files
|
| Mon, 26 Sep 2005 08:50:21 +0200 |
obua |
tuned
|
changeset |
files
|
| Mon, 26 Sep 2005 08:49:50 +0200 |
obua |
added ROOT.ML
|
changeset |
files
|
| Mon, 26 Sep 2005 08:41:24 +0200 |
haftmann |
adjusted web link
|
changeset |
files
|
| Mon, 26 Sep 2005 02:27:59 +0200 |
obua |
added entry for running HOLLight
|
changeset |
files
|
| Mon, 26 Sep 2005 02:27:14 +0200 |
obua |
fixed disambiguation problem
|
changeset |
files
|
| Mon, 26 Sep 2005 02:06:44 +0200 |
obua |
added Drule.disambiguate_frees : thm -> thm
|
changeset |
files
|
| Sun, 25 Sep 2005 23:36:14 +0200 |
wenzelm |
zero_var_inst: replace loose bounds :000 etc.;
|
changeset |
files
|
| Sun, 25 Sep 2005 20:24:23 +0200 |
wenzelm |
* Hyperreal: A theory of Taylor series.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:24:10 +0200 |
wenzelm |
more;
|
changeset |
files
|
| Sun, 25 Sep 2005 20:19:31 +0200 |
berghofe |
eq_codegen now ensures that code for bool type is generated.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:17:44 +0200 |
berghofe |
Fixed print mode problem in test_term.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:17:13 +0200 |
berghofe |
Added ExecutableSet and Taylor.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:15:29 +0200 |
berghofe |
Now uses set implementation from ExecutableSet.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:14:39 +0200 |
berghofe |
Added Taylor.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:14:16 +0200 |
berghofe |
Formalization of Taylor series by Lukas Bulwahn and
|
changeset |
files
|
| Sun, 25 Sep 2005 20:12:59 +0200 |
berghofe |
Added ExecutableSet.
|
changeset |
files
|
| Sun, 25 Sep 2005 20:12:26 +0200 |
berghofe |
New theory for implementing finite sets by lists.
|
changeset |
files
|
| Sun, 25 Sep 2005 01:12:49 +0200 |
webertj |
sat_solver.ML not loaded anymore (already loaded by Refute.thy)
|
changeset |
files
|
| Sat, 24 Sep 2005 23:55:17 +0200 |
obua |
set show_types and show_sorts during import
|
changeset |
files
|
| Sat, 24 Sep 2005 21:13:15 +0200 |
nipkow |
a few new filter lemmas
|
changeset |
files
|
| Sat, 24 Sep 2005 16:43:41 +0200 |
obua |
HOL4-Import: map ONTO to Fun.surj
|
changeset |
files
|
| Sat, 24 Sep 2005 13:54:35 +0200 |
webertj |
cnf_struct renamed to cnf
|
changeset |
files
|
| Sat, 24 Sep 2005 13:26:40 +0200 |
obua |
remove debug clutter
|
changeset |
files
|
| Sat, 24 Sep 2005 13:11:05 +0200 |
obua |
preliminary fix of HOL build problem
|
changeset |
files
|
| Sat, 24 Sep 2005 10:47:22 +0200 |
obua |
bug fix
|
changeset |
files
|
| Sat, 24 Sep 2005 07:57:50 +0200 |
webertj |
replay_proof optimized: now performs backwards proof search
|
changeset |
files
|
| Sat, 24 Sep 2005 07:21:46 +0200 |
webertj |
code reformatted and restructured, many minor modifications
|
changeset |
files
|
| Sat, 24 Sep 2005 07:10:57 +0200 |
webertj |
bugfix in "zchaff_with_proofs"
|
changeset |
files
|
| Sat, 24 Sep 2005 02:53:08 +0200 |
webertj |
parse_std_result_file renamed to read_std_result_file
|
changeset |
files
|
| Fri, 23 Sep 2005 23:28:59 +0200 |
webertj |
new sat tactic
|
changeset |
files
|
| Fri, 23 Sep 2005 22:58:50 +0200 |
webertj |
new sat tactic imports resolution proofs from zChaff
|
changeset |
files
|
| Fri, 23 Sep 2005 22:49:25 +0200 |
obua |
fix
|
changeset |
files
|
| Fri, 23 Sep 2005 22:31:22 +0200 |
wenzelm |
simprocs: pattern now "x" (the proc is supposed to discriminate faster than Pattern.match);
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:55 +0200 |
wenzelm |
tuned msg;
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:54 +0200 |
wenzelm |
added mk_solver';
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:53 +0200 |
wenzelm |
Simplifier.inherit_bounds;
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:52 +0200 |
wenzelm |
adm_tac/cont_tacRs: proper simpset;
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:51 +0200 |
wenzelm |
Provers/Arith/fast_lin_arith.ML: Simplifier.inherit_bounds;
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:50 +0200 |
wenzelm |
tuned order of targets;
|
changeset |
files
|
| Fri, 23 Sep 2005 22:21:49 +0200 |
wenzelm |
Provers/cancel_sums.ML: Simplifier.inherit_bounds;
|
changeset |
files
|
| Fri, 23 Sep 2005 21:02:13 +0200 |
webertj |
some typos in comments fixed
|
changeset |
files
|
| Fri, 23 Sep 2005 20:13:54 +0200 |
obua |
1) fixed bug in type_introduction: first stage uses different namespace than second stage
|
changeset |
files
|
| Fri, 23 Sep 2005 18:47:47 +0200 |
wenzelm |
removed doc/index.html from distribution (now produced by website);
|
changeset |
files
|
| Fri, 23 Sep 2005 17:06:23 +0200 |
haftmann |
mkdir -p for symlinks
|
changeset |
files
|
| Fri, 23 Sep 2005 16:05:42 +0200 |
nipkow |
rules -> iprover
|
changeset |
files
|
| Fri, 23 Sep 2005 16:05:10 +0200 |
webertj |
spaces inserted in header
|
changeset |
files
|
| Fri, 23 Sep 2005 16:01:45 +0200 |
webertj |
header (title/ID) added
|
changeset |
files
|
| Fri, 23 Sep 2005 15:45:12 +0200 |
webertj |
typo fixed: rufute -> refute
|
changeset |
files
|
| Fri, 23 Sep 2005 15:38:22 +0200 |
schirmer |
bugfix in record_tr'
|
changeset |
files
|
| Fri, 23 Sep 2005 15:32:42 +0200 |
wenzelm |
method 'rules' renamed to 'iprover', which does *not* retrieve theorems from the Internet;
|
changeset |
files
|
| Fri, 23 Sep 2005 14:55:28 +0200 |
wenzelm |
Id;
|
changeset |
files
|
| Fri, 23 Sep 2005 13:20:47 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 23 Sep 2005 10:26:07 +0200 |
paulson |
changed defaults
|
changeset |
files
|
| Fri, 23 Sep 2005 10:25:55 +0200 |
paulson |
ATP linkup
|
changeset |
files
|
| Fri, 23 Sep 2005 10:01:14 +0200 |
obua |
replay type_introduction fix
|
changeset |
files
|
| Fri, 23 Sep 2005 09:00:19 +0200 |
haftmann |
temporarily re-introduced overwrite_warn
|
changeset |
files
|
| Fri, 23 Sep 2005 00:52:13 +0200 |
obua |
add debug messages
|
changeset |
files
|
| Fri, 23 Sep 2005 00:11:10 +0200 |
nipkow |
renamed rules to iprover
|
changeset |
files
|
| Fri, 23 Sep 2005 00:10:58 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Thu, 22 Sep 2005 23:56:15 +0200 |
nipkow |
renamed rules to iprover
|
changeset |
files
|
| Thu, 22 Sep 2005 23:55:42 +0200 |
nipkow |
fix because of list lemmas
|
changeset |
files
|
| Thu, 22 Sep 2005 23:43:55 +0200 |
nipkow |
renamed "rules" to "iprover"
|
changeset |
files
|
| Thu, 22 Sep 2005 19:06:34 +0200 |
huffman |
added theorem adm_ball
|
changeset |
files
|
| Thu, 22 Sep 2005 19:06:05 +0200 |
huffman |
cleaned up
|
changeset |
files
|
| Thu, 22 Sep 2005 18:59:41 +0200 |
huffman |
HOLCF theorem naming conventions
|
changeset |
files
|
| Thu, 22 Sep 2005 14:09:48 +0200 |
paulson |
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
|
changeset |
files
|
| Thu, 22 Sep 2005 14:02:14 +0200 |
nipkow |
Fix because of new lemma in List
|
changeset |
files
|
| Thu, 22 Sep 2005 13:52:55 +0200 |
webertj |
solver "auto" does not reverse the list of solvers anymore
|
changeset |
files
|
| Thu, 22 Sep 2005 07:56:16 +0200 |
haftmann |
added fold_map_graph
|
changeset |
files
|
| Thu, 22 Sep 2005 07:56:04 +0200 |
haftmann |
added fold_map_table
|
changeset |
files
|
| Thu, 22 Sep 2005 00:30:31 +0200 |
isatest |
only show trunk in Changelog (kleing)
|
changeset |
files
|
| Wed, 21 Sep 2005 22:01:09 +0200 |
webertj |
zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore
|
changeset |
files
|
| Wed, 21 Sep 2005 21:01:27 +0200 |
wenzelm |
echo HOL_USEDIR_OPTIONS;
|
changeset |
files
|
| Wed, 21 Sep 2005 21:00:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 21 Sep 2005 20:26:45 +0200 |
wenzelm |
PROOFGENERAL_OPTIONS: smart fall-back on plain emacs (back again);
|
changeset |
files
|
| Wed, 21 Sep 2005 20:16:35 +0200 |
wenzelm |
updated for Isabelle2005;
|
changeset |
files
|
| Wed, 21 Sep 2005 20:16:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 21 Sep 2005 19:16:16 +0200 |
wenzelm |
updated for Isabelle2005;
|
changeset |
files
|