1999-08-26 paulson 1999-08-26 extra syntax for JN, making it more like UN
1999-08-26 paulson 1999-08-26 a little tidying; also FIXED BAD TYPE in INTER1, UNION1
1999-08-25 wenzelm 1999-08-25 proper bootstrap of HOL theory and packages;
1999-08-25 wenzelm 1999-08-25 expand_classes renamed to intro_classes;
1999-08-25 wenzelm 1999-08-25 proper bootstrap of IFOL/FOL theories and packages;
1999-08-25 wenzelm 1999-08-25 proper setup of GlobalClaset data;
1999-08-25 wenzelm 1999-08-25 improved msg;
1999-08-25 wenzelm 1999-08-25 fixed arity;
1999-08-25 wenzelm 1999-08-25 expand_classes renamed to intro_classes;
1999-08-25 wenzelm 1999-08-25 TPHOLs99;
1999-08-25 berghofe 1999-08-25 Removed "Adding axioms ..." message.
1999-08-25 wenzelm 1999-08-25 hide private parts;
1999-08-25 paulson 1999-08-25 another snapshot
1999-08-25 paulson 1999-08-25 arguably clearer definition of the inductive case of leads-to. No proofs had to be changed...
1999-08-25 paulson 1999-08-25 tidied
1999-08-25 paulson 1999-08-25 new guarantees laws; also better natural deduction style for old ones
1999-08-25 paulson 1999-08-25 renamed some theorems; also better natural deduction style for old ones
1999-08-25 paulson 1999-08-25 project constants
1999-08-25 paulson 1999-08-25 many "project" laws
1999-08-25 paulson 1999-08-25 new guarantees laws; also better natural deduction style for old ones
1999-08-25 paulson 1999-08-25 split_paired_Eps and lemmas
1999-08-25 paulson 1999-08-25 new theorem inv_f_eq
1999-08-24 wenzelm 1999-08-24 %dir;
1999-08-24 wenzelm 1999-08-24 tuned;
1999-08-24 wenzelm 1999-08-24 draft release;
1999-08-24 wenzelm 1999-08-24 Real/Real.thy main entry point;
1999-08-24 wenzelm 1999-08-24 isar: no_pos flag;
1999-08-24 wenzelm 1999-08-24 fixed add_sect etc.;
1999-08-24 wenzelm 1999-08-24 ??thesis: include params;
1999-08-24 wenzelm 1999-08-24 print_mode activated again;
1999-08-24 wenzelm 1999-08-24 fixed intro_elim_tac;
1999-08-23 wenzelm 1999-08-23 record_simproc;
1999-08-23 wenzelm 1999-08-23 tuned;
1999-08-23 wenzelm 1999-08-23 record_simproc;
1999-08-23 berghofe 1999-08-23 Some changes in sections about Sum and Nat.
1999-08-23 nipkow 1999-08-23 simplifier flex heads.
1999-08-23 nipkow 1999-08-23 Now rewrite rules with flexible heads are allowed.
1999-08-23 wenzelm 1999-08-23 isatool expandshort;
1999-08-23 wenzelm 1999-08-23 tuned;
1999-08-23 berghofe 1999-08-23 Moved sum_case to theory HOL/Datatype.
1999-08-23 wenzelm 1999-08-23 tuned;
1999-08-23 nipkow 1999-08-23 Corrected two busg in the simplifier.
1999-08-22 wenzelm 1999-08-22 \indexisarreg;
1999-08-22 wenzelm 1999-08-22 \VVar;
1999-08-22 wenzelm 1999-08-22 checkpoint;
1999-08-22 wenzelm 1999-08-22 tuned; fixed HOL-Real;
1999-08-21 wenzelm 1999-08-21 real numerals;
1999-08-21 wenzelm 1999-08-21 added HOL-Real; made relocatable;
1999-08-20 wenzelm 1999-08-20 echo ML_PLATFORM;
1999-08-20 wenzelm 1999-08-20 activate example;
1999-08-20 wenzelm 1999-08-20 delcongs [if_weak_cong];
1999-08-20 wenzelm 1999-08-20 print_context;
1999-08-20 wenzelm 1999-08-20 eliminated HOL-AxClasses target;
1999-08-20 wenzelm 1999-08-20 intro (no +);
1999-08-20 wenzelm 1999-08-20 mucke -res;
1999-08-20 wenzelm 1999-08-20 if_svc_enabled;
1999-08-20 wenzelm 1999-08-20 AxClasses, Isar_examples;
1999-08-20 wenzelm 1999-08-20 intro/elim: REPEAT1;
1999-08-20 paulson 1999-08-20 new theories RealBin, RealInt, RealPow
1999-08-19 wenzelm 1999-08-19 * HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;