1999-02-03 paulson 1999-02-03 tidied; added thy_load.ML
1999-02-03 paulson 1999-02-03 tidied, with left_inverse & right_inverse as default simprules
1999-02-03 paulson 1999-02-03 auto update
1999-02-03 paulson 1999-02-03 inj
1999-02-03 paulson 1999-02-03 documented typecheck_tac, etc
1999-02-03 paulson 1999-02-03 standard spelling: type-checking
1999-02-03 paulson 1999-02-03 inj is now a translation of inj_on
1999-02-03 paulson 1999-02-03 standard spelling: type-checking
1999-02-01 paulson 1999-02-01 a bit of tidying
1999-01-30 wenzelm 1999-01-30 Theory loader primitives.
1999-01-29 oheimb 1999-01-29 corrected output of symbols for several (probably not all) relevant functions moved print_mode to ROOT.ML
1999-01-29 oheimb 1999-01-29 renamed space2 to spacespace prepared switch for escaped output of symbols (used for ProofGeneral in connection with the x-symbol package)
1999-01-29 oheimb 1999-01-29 corrected output of symbols for several (probably not all) relevant functions
1999-01-29 oheimb 1999-01-29 moved print_mode to ROOT.ML
1999-01-29 paulson 1999-01-29 expandshort
1999-01-29 paulson 1999-01-29 expandshort
1999-01-29 paulson 1999-01-29 tidied
1999-01-28 paulson 1999-01-28 tidied
1999-01-28 paulson 1999-01-28 constdefs
1999-01-28 paulson 1999-01-28 tidying
1999-01-27 nipkow 1999-01-27 arith_tac for min/max
1999-01-27 wenzelm 1999-01-27 *** empty log message ***
1999-01-27 paulson 1999-01-27 ZF typechecking
1999-01-27 paulson 1999-01-27 automatic insertion of datatype intr rules into claset
1999-01-27 paulson 1999-01-27 new typechecking solver for the simplifier
1999-01-25 wenzelm 1999-01-25 tuned;
1999-01-24 nipkow 1999-01-24 Fixed a bug in lin.arith.
1999-01-22 wenzelm 1999-01-22 tuned;
1999-01-22 wenzelm 1999-01-22 tuned;
1999-01-20 wenzelm 1999-01-20 isabelle.in.tum.de;
1999-01-20 wenzelm 1999-01-20 http://isabelle.in.tum.de/dist/;
1999-01-20 paulson 1999-01-20 renamed variables for clarity
1999-01-20 wenzelm 1999-01-20 changed Minho mirror;
1999-01-19 paulson 1999-01-19 tidied freeness reasoning
1999-01-19 paulson 1999-01-19 freeness reasoning: T.free_iffs
1999-01-19 wenzelm 1999-01-19 tuned;
1999-01-19 paulson 1999-01-19 removal of the (thm list) argument of mk_cases
1999-01-19 paulson 1999-01-19 tidied; added dest_eq
1999-01-19 paulson 1999-01-19 simplified thanks to the arithmetic prover
1999-01-19 paulson 1999-01-19 updated comments
1999-01-19 paulson 1999-01-19 a simplification by G Bella
1999-01-18 wenzelm 1999-01-18 structure Graph = Graph;
1999-01-18 wenzelm 1999-01-18 GraphFun (generic directed graphs); Graph (graphs indexed by strings);
1999-01-18 wenzelm 1999-01-18 added General/graph.ML: generic direct graphs;
1999-01-15 oheimb 1999-01-15 removed empty line (in case of empty begin_state marker) before Level line added printing of subgoals number in Level line
1999-01-14 nipkow 1999-01-14 Removed superfluous arith rules from metric_simps
1999-01-14 nipkow 1999-01-14 More Arith.
1999-01-14 nipkow 1999-01-14 Fixed old bug: selection of constant to be split should depend not just on the name but also on the type.
1999-01-14 nipkow 1999-01-14 nat_arith_tac -> arith_tac
1999-01-14 nipkow 1999-01-14 More arith refinements.
1999-01-14 wenzelm 1999-01-14 tuned README;
1999-01-14 wenzelm 1999-01-14 Pure/General/symbol.ML;
1999-01-14 wenzelm 1999-01-14 tuned;
1999-01-13 paulson 1999-01-13 deleted the appendices because documentation exists in the HOL and ZF manuals
1999-01-13 paulson 1999-01-13 defined dquotesoff
1999-01-13 paulson 1999-01-13 new manual ZF
1999-01-13 paulson 1999-01-13 the separate FOL and ZF logics manual, with new material on datatypes and inductive definitions
1999-01-13 paulson 1999-01-13 removal of FOL and ZF
1999-01-13 paulson 1999-01-13 minor updates on inductive definitions and datatypes
1999-01-13 wenzelm 1999-01-13 fixed titles;