2002-01-11 wenzelm 2002-01-11 Isabelle2002 (January 2002);
2002-01-11 wenzelm 2002-01-11 removed obsolete isamode.ML;
2002-01-11 wenzelm 2002-01-11 tuned;
2002-01-11 wenzelm 2002-01-11 #!/usr/bin/env bash;
2002-01-11 wenzelm 2002-01-11 replace gen_all by forall_elim_vars_safe;
2002-01-11 wenzelm 2002-01-11 improved forall_elim_vars_safe (no longer invents new indexes);
2002-01-11 wenzelm 2002-01-11 lemmas (in ACe) AC;
2002-01-11 wenzelm 2002-01-11 tuned;
2002-01-11 wenzelm 2002-01-11 IsarThy.theorems_i;
2002-01-11 wenzelm 2002-01-11 moved setmksimps to Main!
2002-01-11 wenzelm 2002-01-11 have_thmss vs. have_thmss_i; with_thmss vs. with_thmss_i;
2002-01-11 wenzelm 2002-01-11 clarified/added theorems(_i) vs. locale_theorems(_i); clarified IsarThy.apply_theorems_i; localized smart_theorems, declare_theorems; removed declare_theorems_i;
2002-01-11 wenzelm 2002-01-11 localized 'lemmas', 'theorems', 'declare';
2002-01-11 wenzelm 2002-01-11 have_thmss vs. have_thmss_i;
2002-01-11 wenzelm 2002-01-11 kind: ignore "";
2002-01-11 wenzelm 2002-01-11 IsarThy.theorems_i;
2002-01-11 wenzelm 2002-01-11 clarified IsarThy.apply_theorems_i;
2002-01-11 wenzelm 2002-01-11 * Pure: localized 'lemmas', 'theorems', 'declare';
2002-01-10 wenzelm 2002-01-10 removed add_thmss; added have_thmss(_i);
2002-01-10 wenzelm 2002-01-10 tuned;
2002-01-10 wenzelm 2002-01-10 export_single;
2002-01-10 wenzelm 2002-01-10 refine_tac: Tactic.norm_hhf_tac before trying rule; global_qed: uses Locale.add_thmss_hybrid, tuned;
2002-01-10 wenzelm 2002-01-10 add_thmss_hybrid;
2002-01-10 wenzelm 2002-01-10 export multi_theorem(_i), locale_multi_theorem(_i);
2002-01-10 paulson 2002-01-10 stylistic changes
2002-01-10 nipkow 2002-01-10 *** empty log message ***
2002-01-10 wenzelm 2002-01-10 locales: hide base name of exported version;
2002-01-10 wenzelm 2002-01-10 simplified theorem(_i); smart_multi_theorem;
2002-01-10 wenzelm 2002-01-10 IsarThy.smart_multi_theorem;
2002-01-10 wenzelm 2002-01-10 added hide_thms;
2002-01-10 wenzelm 2002-01-10 simplified IsarThy.theorem_i;
2002-01-10 wenzelm 2002-01-10 qualified exports from locales;
2002-01-09 wenzelm 2002-01-09 obsolete;
2002-01-09 wenzelm 2002-01-09 converted theory Transitive_Closure;
2002-01-09 wenzelm 2002-01-09 * added \<euro> symbol; * HOL-Hyperreal is now a logic image; * isatool latex no longer depends on changed TEXINPUTS;
2002-01-09 wenzelm 2002-01-09 no longer requires TEXINPUTS;
2002-01-09 wenzelm 2002-01-09 isatool latex -o sty;
2002-01-09 wenzelm 2002-01-09 removed TEXINPUTS;
2002-01-09 wenzelm 2002-01-09 updated;
2002-01-09 wenzelm 2002-01-09 tuned;
2002-01-09 wenzelm 2002-01-09 updated;
2002-01-09 wenzelm 2002-01-09 tuned;
2002-01-09 wenzelm 2002-01-09 updated;
2002-01-09 wenzelm 2002-01-09 tuned;
2002-01-09 wenzelm 2002-01-09 tuned message;
2002-01-09 paulson 2002-01-09 changed the index sort key from |-| to just |- because pdflatex can't cope with the two ||s in the index entry
2002-01-08 wenzelm 2002-01-08 HOL-Hyperreal produces an image (again);
2002-01-08 wenzelm 2002-01-08 dependencies for "typedef" image;
2002-01-08 wenzelm 2002-01-08 improved arrangement of "typedef" images;
2002-01-08 wenzelm 2002-01-08 no_document use_thy "While_Combinator";
2002-01-08 wenzelm 2002-01-08 tuned;
2002-01-08 wenzelm 2002-01-08 tuned;
2002-01-08 wenzelm 2002-01-08 tuned;
2002-01-08 wenzelm 2002-01-08 updated;
2002-01-08 wenzelm 2002-01-08 tuned;
2002-01-08 wenzelm 2002-01-08 \part{Elementary Techniques};
2002-01-08 wenzelm 2002-01-08 \chapter{The Basics};
2002-01-08 paulson 2002-01-08 Added some simprules proofs. Converted theories CardinalArith and OrdQuant to Isar style
2002-01-08 wenzelm 2002-01-08 updated;
2002-01-08 wenzelm 2002-01-08 tuned;