1999-09-01 wenzelm 1999-09-01 removed the_fact; added pretty_thms; fix: common constraints; renamed "facts" to "this"; print_state: tuned "Using facts";
1999-09-01 wenzelm 1999-09-01 fix: common constraints;
1999-09-01 wenzelm 1999-09-01 added store/bind_thms;
1999-09-01 wenzelm 1999-09-01 added theorems; improved files;
1999-09-01 wenzelm 1999-09-01 added theorems; begin_theory: implicit files;
1999-09-01 wenzelm 1999-09-01 isar: avoid verbose goal responses;
1999-09-01 wenzelm 1999-09-01 structure Termtab;
1999-09-01 wenzelm 1999-09-01 smart_store_thms;
1999-09-01 wenzelm 1999-09-01 PureThy.smart_store_thms;
1999-09-01 paulson 1999-09-01 tidied some proofs
1999-09-01 paulson 1999-09-01 tidied
1999-08-31 paulson 1999-08-31 tidied
1999-08-31 paulson 1999-08-31 new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration for the overloading of <, while .ML file gets proofs about renaming constants
1999-08-31 paulson 1999-08-31 changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
1999-08-30 wenzelm 1999-08-30 proper calculation / induction;
1999-08-30 wenzelm 1999-08-30 tuned;
1999-08-30 wenzelm 1999-08-30 OF: "_" as argument;
1999-08-30 wenzelm 1999-08-30 clean: include HOL-Real-ex;
1999-08-30 wenzelm 1999-08-30 auto: CHANGED;
1999-08-30 paulson 1999-08-30 make it actually RUN the real examples
1999-08-30 paulson 1999-08-30 new directory HOL/Real/ex of real examples
1999-08-30 wenzelm 1999-08-30 'iff' attribute;
1999-08-30 wenzelm 1999-08-30 'arith' method;
1999-08-30 wenzelm 1999-08-30 '_' theorem; back: only latest command;
1999-08-30 wenzelm 1999-08-30 tuned;
1999-08-30 paulson 1999-08-30 new results for localTo
1999-08-30 paulson 1999-08-30 a new theorem
1999-08-30 wenzelm 1999-08-30 tuned;
1999-08-29 wenzelm 1999-08-29 added MutilatedCheckerboard;
1999-08-29 wenzelm 1999-08-29 added Isar_examples/MutilatedCheckerboard.thy;
1999-08-29 wenzelm 1999-08-29 The Mutilated Chess Board Problem -- Isar'ized version of HOL/Inductive/Mutil;
1999-08-27 wenzelm 1999-08-27 tuned;
1999-08-27 wenzelm 1999-08-27 thm "_" = asm_rl;
1999-08-27 paulson 1999-08-27 tidied
1999-08-27 paulson 1999-08-27 use of bij, new theorems, etc.
1999-08-27 paulson 1999-08-27 the bij predicate forced renaming of a variable bij
1999-08-27 paulson 1999-08-27 tidied, allowing pattern-matching in defs of prat_add and prat_mult
1999-08-27 paulson 1999-08-27 tidied, allowing pattern-matching in defs of zadd and zmult
1999-08-27 paulson 1999-08-27 the bij predicate (at last)
1999-08-27 wenzelm 1999-08-27 better timing information;
1999-08-27 wenzelm 1999-08-27 oops;
1999-08-27 wenzelm 1999-08-27 *** empty log message ***
1999-08-26 wenzelm 1999-08-26 tuned;
1999-08-26 wenzelm 1999-08-26 iff_attrib_setup;
1999-08-26 wenzelm 1999-08-26 improved back, help;
1999-08-26 wenzelm 1999-08-26 print_help;
1999-08-26 wenzelm 1999-08-26 back: recur flag;
1999-08-26 paulson 1999-08-26 a bit further with property (1)
1999-08-26 paulson 1999-08-26 changed "guar" back to "guarantees" (sorry) and FIXED ITS PRECEDENCE
1999-08-26 paulson 1999-08-26 new destruction rules
1999-08-26 paulson 1999-08-26 new laws; changed "guar" back to "guarantees" (sorry)
1999-08-26 paulson 1999-08-26 changed "guar" back to "guarantees" (sorry)
1999-08-26 paulson 1999-08-26 more Join rules including AC-rules
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;