berghofe [Fri, 16 Jul 1999 14:03:03 +0200] rev 7018
Infinitely branching trees.
berghofe [Fri, 16 Jul 1999 13:25:45 +0200] rev 7017
Replaced datatype_info by datatype_info_err.
berghofe [Fri, 16 Jul 1999 13:24:41 +0200] rev 7016
- Now also supports arbitrarily branching datatypes.
- Fixed bug (in some rare cases, recursive constants were
inconsistently typed in different primrec equations).
berghofe [Fri, 16 Jul 1999 12:14:04 +0200] rev 7015
- Datatype package now also supports arbitrarily branching datatypes
(using function types).
- Added new simplification procedure for proving distinctness of
constructors.
- dtK is now a reference.
berghofe [Fri, 16 Jul 1999 12:09:48 +0200] rev 7014
Added some definitions and theorems needed for the
construction of datatypes involving function types.
berghofe [Fri, 16 Jul 1999 12:02:06 +0200] rev 7013
Some rather large datatype examples (from John Harrison).
wenzelm [Thu, 15 Jul 1999 17:54:58 +0200] rev 7012
improved print_thms;
wenzelm [Thu, 15 Jul 1999 17:53:28 +0200] rev 7011
export init_state;
end_proof: reset goal_facts;
paulson [Thu, 15 Jul 1999 10:34:37 +0200] rev 7010
more renaming of theorems from _nat to _int (corresponding to a function that
was similarly renamed some time ago
Also new theorem zmult_int
paulson [Thu, 15 Jul 1999 10:34:00 +0200] rev 7009
more renaming of theorems from _nat to _int (corresponding to a function that
was similarly renamed some time ago
paulson [Thu, 15 Jul 1999 10:33:16 +0200] rev 7008
qed_goal -> Goal; new theorems nat_le_0, nat_le_eq_zle and zdiff_int
paulson [Thu, 15 Jul 1999 10:27:54 +0200] rev 7007
qed_goal -> Goal
wenzelm [Wed, 14 Jul 1999 13:32:21 +0200] rev 7006
tuned;
wenzelm [Wed, 14 Jul 1999 13:07:09 +0200] rev 7005
tuned comments;
wenzelm [Wed, 14 Jul 1999 13:06:08 +0200] rev 7004
tuned contradiction method;
improved comments;
wenzelm [Wed, 14 Jul 1999 13:05:46 +0200] rev 7003
improved comment;
wenzelm [Wed, 14 Jul 1999 13:05:28 +0200] rev 7002
more marg_comments;
wenzelm [Wed, 14 Jul 1999 12:28:12 +0200] rev 7001
Deriving rules in Isabelle;
paulson [Wed, 14 Jul 1999 10:41:33 +0200] rev 7000
rewrite add1_zle_eq is no longer in the default simpset
paulson [Wed, 14 Jul 1999 10:40:51 +0200] rev 6999
optimization for division by powers of 2
paulson [Wed, 14 Jul 1999 10:40:11 +0200] rev 6998
new montonicity theorems
paulson [Wed, 14 Jul 1999 10:39:26 +0200] rev 6997
new constant folding rewrites
wenzelm [Tue, 13 Jul 1999 13:54:08 +0200] rev 6996
handle cgoal;
wenzelm [Tue, 13 Jul 1999 13:53:34 +0200] rev 6995
added mk_cgoal, assume_goal;
wenzelm [Tue, 13 Jul 1999 12:32:22 +0200] rev 6994
same_tac;
paulson [Tue, 13 Jul 1999 10:45:47 +0200] rev 6993
change to force (m div 0 = 0)
paulson [Tue, 13 Jul 1999 10:45:09 +0200] rev 6992
many new theorems
paulson [Tue, 13 Jul 1999 10:44:45 +0200] rev 6991
renamed inj_nat to inj_int
paulson [Tue, 13 Jul 1999 10:44:13 +0200] rev 6990
new monotonicity theorems
paulson [Tue, 13 Jul 1999 10:43:31 +0200] rev 6989
new theorem zmult_eq_0_iff
paulson [Tue, 13 Jul 1999 10:42:31 +0200] rev 6988
renamed sort "numeral" to "number"
paulson [Tue, 13 Jul 1999 10:41:59 +0200] rev 6987
simplified the <= monotonicity proof
wenzelm [Mon, 12 Jul 1999 22:29:38 +0200] rev 6986
local qeds: print rule;
wenzelm [Mon, 12 Jul 1999 22:29:17 +0200] rev 6985
added show_hyps flag;
wenzelm [Mon, 12 Jul 1999 22:28:56 +0200] rev 6984
local qed; print rule;
wenzelm [Mon, 12 Jul 1999 22:28:38 +0200] rev 6983
term/prop: include number;
method args: exlude method meta chars;
wenzelm [Mon, 12 Jul 1999 22:27:51 +0200] rev 6982
added show_hyps flag;
local qed: print rule;
wenzelm [Mon, 12 Jul 1999 22:27:20 +0200] rev 6981
export assumption_tac;
local qeds: print rule;
same_tac: actually insert rules, !! bind vars;
wenzelm [Mon, 12 Jul 1999 22:25:39 +0200] rev 6980
removed merge_theories;
wenzelm [Mon, 12 Jul 1999 22:25:19 +0200] rev 6979
removed metacuts_tac;
wenzelm [Mon, 12 Jul 1999 22:23:59 +0200] rev 6978
tmp_path: *add* path;
wenzelm [Mon, 12 Jul 1999 22:23:31 +0200] rev 6977
thms_containing: undeclared consts error;
wenzelm [Mon, 12 Jul 1999 22:23:07 +0200] rev 6976
removed pretty_thm_no_hyps (again);
wenzelm [Mon, 12 Jul 1999 21:51:47 +0200] rev 6975
removed merge_theories;
wenzelm [Mon, 12 Jul 1999 10:38:31 +0200] rev 6974
may get BASH_PATH etc. from env;
paulson [Mon, 12 Jul 1999 10:32:30 +0200] rev 6973
new theorems for the "at most" relation
wenzelm [Mon, 12 Jul 1999 10:02:38 +0200] rev 6972
def: ==;
wenzelm [Sat, 10 Jul 1999 21:58:19 +0200] rev 6971
tuned Interrupt msgs;
wenzelm [Sat, 10 Jul 1999 21:51:25 +0200] rev 6970
pass exn;
wenzelm [Sat, 10 Jul 1999 21:50:49 +0200] rev 6969
handle THM exn;
wenzelm [Sat, 10 Jul 1999 21:48:27 +0200] rev 6968
handle THM/TERM exn;
wenzelm [Sat, 10 Jul 1999 21:46:15 +0200] rev 6967
dup_elim: use try to handle general exn;
wenzelm [Sat, 10 Jul 1999 21:44:26 +0200] rev 6966
handle THM exn;
wenzelm [Sat, 10 Jul 1999 21:43:27 +0200] rev 6965
fixed interrupts (eliminated races);
wenzelm [Sat, 10 Jul 1999 21:41:57 +0200] rev 6964
defer_tac: use try for general exn handling;
wenzelm [Sat, 10 Jul 1999 21:41:05 +0200] rev 6963
Symtab.lookup_multi;
wenzelm [Sat, 10 Jul 1999 21:40:14 +0200] rev 6962
more specific exn;
wenzelm [Sat, 10 Jul 1999 21:38:30 +0200] rev 6961
err_method: pass exn;
nontriv_merge: no handle_error;
wenzelm [Sat, 10 Jul 1999 21:35:08 +0200] rev 6960
prove_goalw_cterm_general: pass exeption;
wenzelm [Sat, 10 Jul 1999 21:34:01 +0200] rev 6959
try/can: pass Interrupt and ERROR;
nth_elem_string: use try;
wenzelm [Fri, 09 Jul 1999 19:11:50 +0200] rev 6958
rmdir pdf;
wenzelm [Fri, 09 Jul 1999 18:59:01 +0200] rev 6957
mono: extra I/E;
wenzelm [Fri, 09 Jul 1999 18:58:05 +0200] rev 6956
mono: AddXI/Es;
wenzelm [Fri, 09 Jul 1999 18:54:55 +0200] rev 6955
type claset: added extra I/E rules;