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;
1999-01-13 paulson 1999-01-13 tidying of datatype and inductive definitions
1999-01-13 wenzelm 1999-01-13 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
1999-01-13 nipkow 1999-01-13 Refined arithmetic.
1999-01-13 paulson 1999-01-13 congruence rules finally use == instead of = and <->
1999-01-13 paulson 1999-01-13 generalized qed_spec_mp code to work for ZF
1999-01-13 paulson 1999-01-13 datatype package improvements
1999-01-13 paulson 1999-01-13 better qed_spec_mp
1999-01-13 nipkow 1999-01-13 Simplified interface.
1999-01-13 nipkow 1999-01-13 Simplified arithmetic.
1999-01-12 wenzelm 1999-01-12 'same' method, 'immediate' proof;
1999-01-12 wenzelm 1999-01-12 tuned msg;
1999-01-12 wenzelm 1999-01-12 SYNC;
1999-01-12 wenzelm 1999-01-12 fixed again;