| 2005-07-15 |
obua |
optimize no_types_needed, remove exception handler
|
changeset |
files
|
| 2005-07-15 |
wenzelm |
tuned;
|
changeset |
files
|
| 2005-07-14 |
dixon |
lucas - slightly cleaned up. Removed redudent copy of Symtab structure.
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
* Improved 'oracle' command -- type-safe;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
no open Logic;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
removed itlist, rev_itlist -- use fold_rev, fold instead;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
replaced itlist by fold_rev;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
replaced itlist by fold_rev;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
use sys_error instead of exception Internal;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
sys_error;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
type-safe 'oracle' command;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
added dest_table;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
invoke_oracle: do not keep theory value, but theory_ref;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
occs no longer infix (structure not open);
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
NameSpace.dest_table avoids duplicated extern;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
with_path;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
removed mk_prodT, mk_not (cf. HOL/hologic.ML);
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
tuned;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
use all files in HOLCF.thy;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
replaced Utils.itlist by fold_rev;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
proper structure;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
use existing Inttab;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
improved oracle setup;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
improved oracle setup;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
removed not_const -- use Not instead;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
HOL.Not;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
HOL.Not;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
new type-safe interface;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
removed FOL/ex/IffOracle.ML;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
obsolete;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
improved 'oracle' command;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
tuned;
|
changeset |
files
|
| 2005-07-14 |
wenzelm |
accomodate change of real_of_XXX;
|
changeset |
files
|
| 2005-07-14 |
obua |
- fixed bug concerning the renaming of axiom names
|
changeset |
files
|
| 2005-07-14 |
haftmann |
added ` combinator
|
changeset |
files
|
| 2005-07-14 |
haftmann |
(fix for smlnj)
|
changeset |
files
|
| 2005-07-13 |
huffman |
simplified proof of cont_Iwhen3
|
changeset |
files
|
| 2005-07-13 |
schirmer |
avoiding even more garbage
|
changeset |
files
|
| 2005-07-13 |
aspinall |
Update PGIP packet handling, fixing unique session identifier.
|
changeset |
files
|
| 2005-07-13 |
avigad |
fixed typos in theorem names
|
changeset |
files
|
| 2005-07-13 |
avigad |
Additions to the Real (and Hyperreal) libraries:
|
changeset |
files
|
| 2005-07-13 |
paulson |
tidied
|
changeset |
files
|
| 2005-07-13 |
aspinall |
Add ISABELLE_PID for proof_general.ML
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
tuned msg;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
added print_state_hook;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
export previous;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
removed ad-hoc atp_hook, cal_atp;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
Toplevel.actual_proof;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
avoid excessive exceptions;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
Graph: fast_string_ord;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
export eq_brl;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
added subtract;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
export eq_rrule;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
removed obsolete delta stuff;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
open ReconPrelim Recon_Transfer;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
open ReconPrelim ReconTranslateProof;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
tuned;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
use Toplevel.print_state_hook instead of adhoc Proof.atp_hook;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
tuned concat_with_and;
|
changeset |
files
|
| 2005-07-13 |
wenzelm |
improved Net interface;
|
changeset |
files
|