wenzelm [Sun, 13 Jan 2002 21:09:17 +0100] rev 12735
added HOL/Real/document/root.tex;
wenzelm [Sun, 13 Jan 2002 19:45:17 +0100] rev 12734
HOL-Real/Complex_Numbers;
wenzelm [Sun, 13 Jan 2002 19:42:30 +0100] rev 12733
Real/Complex_Numbers.thy;
wenzelm [Sat, 12 Jan 2002 22:44:10 +0100] rev 12732
tuned;
wenzelm [Sat, 12 Jan 2002 22:24:09 +0100] rev 12731
tuned;
wenzelm [Sat, 12 Jan 2002 22:17:08 +0100] rev 12730
produce predicate text;
proper checking of defines;
wenzelm [Sat, 12 Jan 2002 22:15:48 +0100] rev 12729
added atomize_cterm;
wenzelm [Sat, 12 Jan 2002 16:55:53 +0100] rev 12728
tuned;
wenzelm [Sat, 12 Jan 2002 16:40:02 +0100] rev 12727
unify_frozen: proper use of maxidx';
declare_elemss: need to unify_elemss beforehand;
wenzelm [Sat, 12 Jan 2002 16:38:42 +0100] rev 12726
paramify_dummies: proper treatment of maxidx;
wenzelm [Sat, 12 Jan 2002 16:37:58 +0100] rev 12725
renamed forall_elim_vars_safe to gen_all;
wenzelm [Fri, 11 Jan 2002 18:49:25 +0100] rev 12724
Isabelle2002 (January 2002);
wenzelm [Fri, 11 Jan 2002 18:07:45 +0100] rev 12723
removed obsolete isamode.ML;
wenzelm [Fri, 11 Jan 2002 18:07:30 +0100] rev 12722
tuned;
wenzelm [Fri, 11 Jan 2002 17:04:49 +0100] rev 12721
#!/usr/bin/env bash;
wenzelm [Fri, 11 Jan 2002 14:53:30 +0100] rev 12720
replace gen_all by forall_elim_vars_safe;
wenzelm [Fri, 11 Jan 2002 14:53:05 +0100] rev 12719
improved forall_elim_vars_safe (no longer invents new indexes);
wenzelm [Fri, 11 Jan 2002 14:44:58 +0100] rev 12718
lemmas (in ACe) AC;
wenzelm [Fri, 11 Jan 2002 14:44:24 +0100] rev 12717
tuned;
wenzelm [Fri, 11 Jan 2002 00:35:03 +0100] rev 12716
IsarThy.theorems_i;
wenzelm [Fri, 11 Jan 2002 00:34:43 +0100] rev 12715
moved setmksimps to Main!
wenzelm [Fri, 11 Jan 2002 00:33:35 +0100] rev 12714
have_thmss vs. have_thmss_i;
with_thmss vs. with_thmss_i;
wenzelm [Fri, 11 Jan 2002 00:32:17 +0100] rev 12713
clarified/added theorems(_i) vs. locale_theorems(_i);
clarified IsarThy.apply_theorems_i;
localized smart_theorems, declare_theorems;
removed declare_theorems_i;
wenzelm [Fri, 11 Jan 2002 00:30:28 +0100] rev 12712
localized 'lemmas', 'theorems', 'declare';
wenzelm [Fri, 11 Jan 2002 00:29:54 +0100] rev 12711
have_thmss vs. have_thmss_i;
wenzelm [Fri, 11 Jan 2002 00:29:25 +0100] rev 12710
kind: ignore "";
wenzelm [Fri, 11 Jan 2002 00:28:43 +0100] rev 12709
IsarThy.theorems_i;
wenzelm [Fri, 11 Jan 2002 00:28:24 +0100] rev 12708
clarified IsarThy.apply_theorems_i;