Tue, 13 Jul 1999 13:53:34 +0200 |
wenzelm |
added mk_cgoal, assume_goal;
|
changeset |
files
|
Tue, 13 Jul 1999 12:32:22 +0200 |
wenzelm |
same_tac;
|
changeset |
files
|
Tue, 13 Jul 1999 10:45:47 +0200 |
paulson |
change to force (m div 0 = 0)
|
changeset |
files
|
Tue, 13 Jul 1999 10:45:09 +0200 |
paulson |
many new theorems
|
changeset |
files
|
Tue, 13 Jul 1999 10:44:45 +0200 |
paulson |
renamed inj_nat to inj_int
|
changeset |
files
|
Tue, 13 Jul 1999 10:44:13 +0200 |
paulson |
new monotonicity theorems
|
changeset |
files
|
Tue, 13 Jul 1999 10:43:31 +0200 |
paulson |
new theorem zmult_eq_0_iff
|
changeset |
files
|
Tue, 13 Jul 1999 10:42:31 +0200 |
paulson |
renamed sort "numeral" to "number"
|
changeset |
files
|
Tue, 13 Jul 1999 10:41:59 +0200 |
paulson |
simplified the <= monotonicity proof
|
changeset |
files
|
Mon, 12 Jul 1999 22:29:38 +0200 |
wenzelm |
local qeds: print rule;
|
changeset |
files
|
Mon, 12 Jul 1999 22:29:17 +0200 |
wenzelm |
added show_hyps flag;
|
changeset |
files
|
Mon, 12 Jul 1999 22:28:56 +0200 |
wenzelm |
local qed; print rule;
|
changeset |
files
|
Mon, 12 Jul 1999 22:28:38 +0200 |
wenzelm |
term/prop: include number;
|
changeset |
files
|
Mon, 12 Jul 1999 22:27:51 +0200 |
wenzelm |
added show_hyps flag;
|
changeset |
files
|
Mon, 12 Jul 1999 22:27:20 +0200 |
wenzelm |
export assumption_tac;
|
changeset |
files
|
Mon, 12 Jul 1999 22:25:39 +0200 |
wenzelm |
removed merge_theories;
|
changeset |
files
|
Mon, 12 Jul 1999 22:25:19 +0200 |
wenzelm |
removed metacuts_tac;
|
changeset |
files
|
Mon, 12 Jul 1999 22:23:59 +0200 |
wenzelm |
tmp_path: *add* path;
|
changeset |
files
|
Mon, 12 Jul 1999 22:23:31 +0200 |
wenzelm |
thms_containing: undeclared consts error;
|
changeset |
files
|
Mon, 12 Jul 1999 22:23:07 +0200 |
wenzelm |
removed pretty_thm_no_hyps (again);
|
changeset |
files
|
Mon, 12 Jul 1999 21:51:47 +0200 |
wenzelm |
removed merge_theories;
|
changeset |
files
|
Mon, 12 Jul 1999 10:38:31 +0200 |
wenzelm |
may get BASH_PATH etc. from env;
|
changeset |
files
|
Mon, 12 Jul 1999 10:32:30 +0200 |
paulson |
new theorems for the "at most" relation
|
changeset |
files
|
Mon, 12 Jul 1999 10:02:38 +0200 |
wenzelm |
def: ==;
|
changeset |
files
|
Sat, 10 Jul 1999 21:58:19 +0200 |
wenzelm |
tuned Interrupt msgs;
|
changeset |
files
|
Sat, 10 Jul 1999 21:51:25 +0200 |
wenzelm |
pass exn;
|
changeset |
files
|
Sat, 10 Jul 1999 21:50:49 +0200 |
wenzelm |
handle THM exn;
|
changeset |
files
|
Sat, 10 Jul 1999 21:48:27 +0200 |
wenzelm |
handle THM/TERM exn;
|
changeset |
files
|
Sat, 10 Jul 1999 21:46:15 +0200 |
wenzelm |
dup_elim: use try to handle general exn;
|
changeset |
files
|
Sat, 10 Jul 1999 21:44:26 +0200 |
wenzelm |
handle THM exn;
|
changeset |
files
|
Sat, 10 Jul 1999 21:43:27 +0200 |
wenzelm |
fixed interrupts (eliminated races);
|
changeset |
files
|
Sat, 10 Jul 1999 21:41:57 +0200 |
wenzelm |
defer_tac: use try for general exn handling;
|
changeset |
files
|
Sat, 10 Jul 1999 21:41:05 +0200 |
wenzelm |
Symtab.lookup_multi;
|
changeset |
files
|
Sat, 10 Jul 1999 21:40:14 +0200 |
wenzelm |
more specific exn;
|
changeset |
files
|
Sat, 10 Jul 1999 21:38:30 +0200 |
wenzelm |
err_method: pass exn;
|
changeset |
files
|
Sat, 10 Jul 1999 21:35:08 +0200 |
wenzelm |
prove_goalw_cterm_general: pass exeption;
|
changeset |
files
|
Sat, 10 Jul 1999 21:34:01 +0200 |
wenzelm |
try/can: pass Interrupt and ERROR;
|
changeset |
files
|
Fri, 09 Jul 1999 19:11:50 +0200 |
wenzelm |
rmdir pdf;
|
changeset |
files
|
Fri, 09 Jul 1999 18:59:01 +0200 |
wenzelm |
mono: extra I/E;
|
changeset |
files
|
Fri, 09 Jul 1999 18:58:05 +0200 |
wenzelm |
mono: AddXI/Es;
|
changeset |
files
|
Fri, 09 Jul 1999 18:54:55 +0200 |
wenzelm |
type claset: added extra I/E rules;
|
changeset |
files
|
Fri, 09 Jul 1999 18:48:54 +0200 |
wenzelm |
added Isar/local_defs.ML;
|
changeset |
files
|
Fri, 09 Jul 1999 18:48:33 +0200 |
wenzelm |
added 'def';
|
changeset |
files
|
Fri, 09 Jul 1999 18:47:56 +0200 |
wenzelm |
added local_def(_i);
|
changeset |
files
|
Fri, 09 Jul 1999 18:47:15 +0200 |
wenzelm |
global_qed: removed alt_name, alt_att;
|
changeset |
files
|
Fri, 09 Jul 1999 18:46:51 +0200 |
wenzelm |
global_qed: removed alt_name, alt_att;
|
changeset |
files
|
Fri, 09 Jul 1999 18:45:15 +0200 |
wenzelm |
added termp;
|
changeset |
files
|
Fri, 09 Jul 1999 18:44:58 +0200 |
wenzelm |
COMP: optional position;
|
changeset |
files
|
Fri, 09 Jul 1999 16:55:20 +0200 |
wenzelm |
write_keywords: default file name;
|
changeset |
files
|
Fri, 09 Jul 1999 16:54:54 +0200 |
wenzelm |
added compose_single;
|
changeset |
files
|
Fri, 09 Jul 1999 16:45:18 +0200 |
wenzelm |
added HOL.trans;
|
changeset |
files
|
Fri, 09 Jul 1999 16:44:55 +0200 |
wenzelm |
removed qed_with;
|
changeset |
files
|
Fri, 09 Jul 1999 10:49:14 +0200 |
paulson |
faster division algorithm; monotonicity of div in 2nd arg
|
changeset |
files
|
Fri, 09 Jul 1999 10:47:42 +0200 |
paulson |
more monotonicity laws for times
|
changeset |
files
|
Fri, 09 Jul 1999 10:45:09 +0200 |
paulson |
products of signs as equivalences
|
changeset |
files
|
Thu, 08 Jul 1999 18:40:43 +0200 |
wenzelm |
-B option;
|
changeset |
files
|
Thu, 08 Jul 1999 18:39:34 +0200 |
wenzelm |
removed old version;
|
changeset |
files
|
Thu, 08 Jul 1999 18:39:08 +0200 |
wenzelm |
tuned indentation;
|
changeset |
files
|
Thu, 08 Jul 1999 18:37:54 +0200 |
wenzelm |
added export_chain;
|
changeset |
files
|
Thu, 08 Jul 1999 18:36:57 +0200 |
wenzelm |
propp: 'concl' patterns;
|
changeset |
files
|