2000-02-05 wenzelm 2000-02-05 -I option;
2000-02-05 wenzelm 2000-02-05 -D PATH: dump generated document sources into PATH;
2000-02-05 wenzelm 2000-02-05 additional tex dump;
2000-02-05 wenzelm 2000-02-05 '.' == by this;
2000-02-04 wenzelm 2000-02-04 misc improvements;
2000-02-04 wenzelm 2000-02-04 added MicroJava/document;
2000-02-04 wenzelm 2000-02-04 added old_symbol_source; tuned;
2000-02-04 wenzelm 2000-02-04 Present.old_symbol_source;
2000-02-04 wenzelm 2000-02-04 tuned;
2000-02-04 wenzelm 2000-02-04 manually load session;
2000-02-04 wenzelm 2000-02-04 tuned syms;
2000-02-04 paulson 2000-02-04 new theorem gcd_add_mult
2000-02-02 wenzelm 2000-02-02 most_general_varify_tfrees all results;
2000-02-02 nipkow 2000-02-02 Rduced Class C <= Class D to C <= D.
2000-02-02 wenzelm 2000-02-02 nat as names; obtain; tuned;
2000-02-02 paulson 2000-02-02 expandshort
2000-02-02 paulson 2000-02-02 new lemma fun_cons_restrict_eq
2000-02-02 paulson 2000-02-02 new theorems by Sidi O. Ehmety
2000-02-01 oheimb 2000-02-01 added forgotten definition of make_imp_tac
2000-02-01 oheimb 2000-02-01 added forgotten rules to make IMPP
2000-02-01 wenzelm 2000-02-01 eliminated nonascii;
2000-01-31 oheimb 2000-01-31 added IMPP to HOL
2000-01-31 paulson 2000-01-31 renamed image_Union_eq -> image_Union
2000-01-31 paulson 2000-01-31 new theorem vimage_Union
2000-01-31 paulson 2000-01-31 new theorem rev_ImageI
2000-01-31 paulson 2000-01-31 various theorems about image and inverse image
2000-01-31 paulson 2000-01-31 Pi_empty1 is a more general simprule than empty_fun
2000-01-30 wenzelm 2000-01-30 rm -f *.aux;
2000-01-29 wenzelm 2000-01-29 simp_all method;
2000-01-28 wenzelm 2000-01-28 eliminated proof script;
2000-01-28 wenzelm 2000-01-28 HEADGOAL;
2000-01-28 wenzelm 2000-01-28 added prefer, defer;
2000-01-28 wenzelm 2000-01-28 added HEADGOAL;
2000-01-28 wenzelm 2000-01-28 added defer, prefer;
2000-01-28 wenzelm 2000-01-28 Drule.instantiate;
2000-01-28 wenzelm 2000-01-28 cp -r;
2000-01-28 wenzelm 2000-01-28 -p option;
2000-01-28 oheimb 2000-01-28 added range_composition (also to simpset)
2000-01-28 oheimb 2000-01-28 added finite_range_updI, finite_range_map_of, finite_range_map_of_override added, also to simpset: override_upd, ran_empty'
2000-01-28 wenzelm 2000-01-28 mkdir: prepare logic session directory;
2000-01-28 oheimb 2000-01-28 added full_nat_induct
2000-01-28 oheimb 2000-01-28 added splitE', also to claset
2000-01-28 oheimb 2000-01-28 added inj_singleton
2000-01-28 oheimb 2000-01-28 added finite_range_imageI
2000-01-28 wenzelm 2000-01-28 replaced FIRSTGOAL by FINDGOAL (backtracking!);
2000-01-28 wenzelm 2000-01-28 maintain standard rules (beware: classical provers provides another version!);
2000-01-28 wenzelm 2000-01-28 replaced FIRSTGOAL by FINDGOAL (backtracking!); improved flexflex handling; tuned sig;
2000-01-28 wenzelm 2000-01-28 tuned sig;
2000-01-28 wenzelm 2000-01-28 map data;
2000-01-28 oheimb 2000-01-28 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
2000-01-28 oheimb 2000-01-28 beautified spacing for binders with symbols syntax, analogous to HOL.thy
2000-01-27 oheimb 2000-01-27 *** empty log message ***
2000-01-26 wenzelm 2000-01-26 'name' etc. include 'number'; attrib: include keyword_sid as name;
2000-01-26 wenzelm 2000-01-26 'name' syntax includes numbers;
2000-01-26 nipkow 2000-01-26 optimized xs[i:=x]!j lemmas.
2000-01-25 wenzelm 2000-01-25 added map, map_st;
2000-01-25 wenzelm 2000-01-25 added map;
2000-01-25 wenzelm 2000-01-25 fallback on PureThy version;
2000-01-25 nipkow 2000-01-25 replaced f : A funcset B by f``A <= B.
2000-01-24 kleing 2000-01-24 reflexivity simp rules