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;
2002-01-08 nipkow 2002-01-08 added filter_filter
2002-01-08 paulson 2002-01-08 #2 to 2
2002-01-08 wenzelm 2002-01-08 syntax "_not_equal";
2002-01-08 wenzelm 2002-01-08 removed (not really necessary, causes too many consistency problems);
2002-01-08 wenzelm 2002-01-08 tuned;
2002-01-07 wenzelm 2002-01-07 getting close to completion;
2002-01-07 wenzelm 2002-01-07 updated;
2002-01-07 wenzelm 2002-01-07 tuned;
2002-01-07 wenzelm 2002-01-07 updated;
2002-01-07 wenzelm 2002-01-07 tuned;
2002-01-07 wenzelm 2002-01-07 tuned deps;
2002-01-07 wenzelm 2002-01-07 tuned;
2002-01-07 wenzelm 2002-01-07 updated;
2002-01-06 wenzelm 2002-01-06 some more ...;
2002-01-06 wenzelm 2002-01-06 "_not_equal" dummy constant;
2002-01-06 wenzelm 2002-01-06 updated;