| Wed, 02 Nov 2005 14:46:51 +0100 |
wenzelm |
dist_eqI: the_context();
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:49 +0100 |
wenzelm |
Sign.const_monomorphic;
|
changeset |
files
|
| Wed, 02 Nov 2005 14:46:47 +0100 |
wenzelm |
Logic.nth_prem;
|
changeset |
files
|
| Wed, 02 Nov 2005 11:02:29 +0100 |
urbanc |
added the collection of lemmas "supp_at"
|
changeset |
files
|
| Tue, 01 Nov 2005 23:55:53 +0100 |
urbanc |
some minor tweaks in some proofs (nothing extraordinary)
|
changeset |
files
|
| Tue, 01 Nov 2005 23:54:29 +0100 |
urbanc |
tunings of some comments (nothing serious)
|
changeset |
files
|
| Mon, 31 Oct 2005 16:35:15 +0100 |
haftmann |
nth_*, fold_index refined
|
changeset |
files
|
| 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
|