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