1999-08-30 wenzelm tuned;
1999-08-30 wenzelm OF: "_" as argument;
1999-08-30 wenzelm clean: include HOL-Real-ex;
1999-08-30 wenzelm auto: CHANGED;
1999-08-30 paulson make it actually RUN the real examples
1999-08-30 paulson new directory HOL/Real/ex of real examples
1999-08-30 wenzelm 'iff' attribute;
1999-08-30 wenzelm 'arith' method;
1999-08-30 wenzelm '_' theorem;
1999-08-30 wenzelm tuned;
1999-08-30 paulson new results for localTo
1999-08-30 paulson a new theorem
1999-08-30 wenzelm tuned;
1999-08-29 wenzelm added MutilatedCheckerboard;
1999-08-29 wenzelm added Isar_examples/MutilatedCheckerboard.thy;
1999-08-29 wenzelm The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
1999-08-27 wenzelm tuned;
1999-08-27 wenzelm thm "_" = asm_rl;
1999-08-27 paulson tidied
1999-08-27 paulson use of bij, new theorems, etc.
1999-08-27 paulson the bij predicate forced renaming of a variable bij
1999-08-27 paulson tidied, allowing pattern-matching in defs of prat_add and prat_mult
1999-08-27 paulson tidied, allowing pattern-matching in defs of zadd and zmult
1999-08-27 paulson the bij predicate (at last)
1999-08-27 wenzelm better timing information;
1999-08-27 wenzelm oops;
1999-08-27 wenzelm *** empty log message ***
1999-08-26 wenzelm tuned;
1999-08-26 wenzelm iff_attrib_setup;
1999-08-26 wenzelm improved back, help;
1999-08-26 wenzelm print_help;
1999-08-26 wenzelm back: recur flag;
1999-08-26 paulson a bit further with property (1)
1999-08-26 paulson changed "guar" back to "guarantees" (sorry) and FIXED ITS PRECEDENCE
1999-08-26 paulson new destruction rules
1999-08-26 paulson new laws; changed "guar" back to "guarantees" (sorry)
1999-08-26 paulson changed "guar" back to "guarantees" (sorry)
1999-08-26 paulson more Join rules including AC-rules
1999-08-26 paulson extra syntax for JN, making it more like UN
1999-08-26 paulson a little tidying; also FIXED BAD TYPE in INTER1, UNION1
1999-08-25 wenzelm proper bootstrap of HOL theory and packages;
1999-08-25 wenzelm expand_classes renamed to intro_classes;
1999-08-25 wenzelm proper bootstrap of IFOL/FOL theories and packages;
1999-08-25 wenzelm proper setup of GlobalClaset data;
1999-08-25 wenzelm improved msg;
1999-08-25 wenzelm fixed arity;
1999-08-25 wenzelm expand_classes renamed to intro_classes;
1999-08-25 wenzelm TPHOLs99;
1999-08-25 berghofe Removed "Adding axioms ..." message.
1999-08-25 wenzelm hide private parts;
1999-08-25 paulson another snapshot
1999-08-25 paulson arguably clearer definition of the inductive case of
1999-08-25 paulson tidied
1999-08-25 paulson new guarantees laws; also better natural deduction style for old ones
1999-08-25 paulson renamed some theorems; also better natural deduction style for old ones
1999-08-25 paulson project constants
1999-08-25 paulson many "project" laws
1999-08-25 paulson new guarantees laws; also better natural deduction style for old ones
1999-08-25 paulson split_paired_Eps and lemmas
1999-08-25 paulson new theorem inv_f_eq
(0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip