| 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
|