2001-06-13 paulson 2001-06-13 New proof of gcd_zero after a change to Divides.ML made the old one fail
2001-06-13 paulson 2001-06-13 a couple of new theorems
2001-06-12 oheimb 2001-06-12 corrected xsymbol/HTML syntax
2001-06-11 berghofe 2001-06-11 Fixed bug in function rebuild.
2001-06-10 paulson 2001-06-10 new GroupTheory example, e.g. the Sylow theorem (preliminary version)
2001-06-09 wenzelm 2001-06-09 tuned
2001-06-09 wenzelm 2001-06-09 tuned Primes theory;
2001-06-09 paulson 2001-06-09 addition of the GREATEST quantifier
2001-06-09 paulson 2001-06-09 renaming of evs in the Fake rule
2001-06-09 paulson 2001-06-09 new material from the Sylow proof
2001-06-09 paulson 2001-06-09 simplified a proof using new dvd rules
2001-06-09 paulson 2001-06-09 moved Primes.thy from NumberTheory to Library
2001-06-08 nipkow 2001-06-08 Removed BCV
2001-06-05 nipkow 2001-06-05 *** empty log message ***
2001-06-05 nipkow 2001-06-05 This is now superseded by MicroJava/BV
2001-06-01 paulson 2001-06-01 renamed # to ## to avoid clashing with List cons
2001-06-01 paulson 2001-06-01 now checks for leading meta-quantifiers and complains, instead of just raising an exception
2001-05-31 wenzelm 2001-05-31 tuned
2001-05-31 wenzelm 2001-05-31 added HOL-CTL;
2001-05-31 wenzelm 2001-05-31 tuned
2001-05-31 paulson 2001-05-31 examples files start from Main instead of various ZF theories
2001-05-31 wenzelm 2001-05-31 invent_names
2001-05-31 bauerg 2001-05-31 added HOL-CTL example;
2001-05-31 oheimb 2001-05-31 added Library/Nat_Infinity.thy and Library/Continuity.thy
2001-05-31 oheimb 2001-05-31 added FOCUS including the One-Element Buffer by Manfred Broy
2001-05-31 oheimb 2001-05-31 added Library/Nat_Infinity.thy and Library/Continuity.thy
2001-05-31 oheimb 2001-05-31 added stream length, map, and filter
2001-05-31 oheimb 2001-05-31 corrected ML names of definitions, added chain_shift
2001-05-31 oheimb 2001-05-31 corrected ML names of definitions
2001-05-31 oheimb 2001-05-31 improved iff_add_global, new function add_rules factoring out common behaviour
2001-05-31 oheimb 2001-05-31 streamlined addIffs/delIffs, added warnings
2001-05-31 oheimb 2001-05-31 replaced Sel_injective_cprod by new injective_fst_snd
2001-05-31 oheimb 2001-05-31 added lub_range_mono and lub_range_shift
2001-05-31 oheimb 2001-05-31 added chain_monofun
2001-05-31 oheimb 2001-05-31 added same_fstI as safe intro rule
2001-05-31 oheimb 2001-05-31 added injective_fst_snd
2001-05-31 oheimb 2001-05-31 added nat_not_singleton (also to simpset)
2001-05-31 oheimb 2001-05-31 added Least_Suc2
2001-05-31 oheimb 2001-05-31 added list_all2_trans
2001-05-31 oheimb 2001-05-31 added weak_coinduct_image
2001-05-31 nipkow 2001-05-31 Allow Suc-numerals as coefficients in lin-arith formulae
2001-05-31 oheimb 2001-05-31 corrected entry for iff attribute
2001-05-30 oheimb 2001-05-30 extended doc for iff attribute
2001-05-30 bauerg 2001-05-30 injectivity of ^;
2001-05-29 paulson 2001-05-29 deleted a needless reference to rtrancl_unfold
2001-05-28 oheimb 2001-05-28 improved handling of space before/after parentheses
2001-05-22 berghofe 2001-05-22 Inductive characterization of wfrec combinator.
2001-05-22 berghofe 2001-05-22 Transitive closure is now defined via "inductive".
2001-05-22 berghofe 2001-05-22 Representing set for type nat is now defined via "inductive".
2001-05-22 berghofe 2001-05-22 Inductive definitions are now introduced earlier in the theory hierarchy.
2001-05-22 paulson 2001-05-22 nat_diff_split_asm, for the assumptions
2001-05-21 paulson 2001-05-21 if_splits and split_if_asm
2001-05-21 paulson 2001-05-21 fixed the X-symbol syntax for lambda
2001-05-21 paulson 2001-05-21 the rest of integer division
2001-05-21 paulson 2001-05-21 X-symbols for set theory
2001-05-21 paulson 2001-05-21 X-symbols for ZF
2001-05-21 paulson 2001-05-21 X-symbols for ZF
2001-05-21 paulson 2001-05-21 X-symbols for set theory
2001-05-21 paulson 2001-05-21 X-symbols for set theory
2001-05-21 paulson 2001-05-21 Division examples