2009-07-24 wenzelm 2009-07-24 structure OldGoals: no pervasive names;
2009-07-24 wenzelm 2009-07-24 renamed functor ProjectRuleFun to Project_Rule; renamed structure ProjectRule to Project_Rule;
2009-07-24 wenzelm 2009-07-24 renamed functor InductFun to Induct;
2009-07-24 wenzelm 2009-07-24 tuned;
2009-07-24 wenzelm 2009-07-24 renamed Pure/tctical.ML to Pure/tactical.ML;
2009-07-24 wenzelm 2009-07-24 eliminated print_goals_without_context -- proper pretty printing;
2009-07-24 wenzelm 2009-07-24 Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
2009-07-24 wenzelm 2009-07-24 removed Formal_Power_Series_Examples (cf. adea7a729c7a);
2009-07-24 wenzelm 2009-07-24 make: keep going by default;
2009-07-23 chaieb 2009-07-23 merged
2009-07-23 chaieb 2009-07-23 merged
2009-07-23 chaieb 2009-07-23 fixed proof --- fact_setprod removed for fact_altdef_nat
2009-07-23 chaieb 2009-07-23 merged
2009-07-23 chaieb 2009-07-23 Vandermonde vs Pochhammer; Hypergeometric series - very basic facts
2009-07-23 chaieb 2009-07-23 More theorems about pochhammer
2009-07-15 chaieb 2009-07-15 Moved theorem binomial_symmetric from Formal_Power_Series to here
2009-07-15 chaieb 2009-07-15 Moved important theorems from FPS_Examples to FPS --- they are not really examples but useful theorems that are being reproved since unnoticed.
2009-07-23 wenzelm 2009-07-23 removed obsolete ML proof tools;
2009-07-23 wenzelm 2009-07-23 more @{theory} antiquotations;
2009-07-23 wenzelm 2009-07-23 eliminated adhoc ML code;
2009-07-23 wenzelm 2009-07-23 misc modernization: proper method setup instead of adhoc ML proofs;
2009-07-23 wenzelm 2009-07-23 global_claset_of;
2009-07-23 wenzelm 2009-07-23 Proper context for simpset_of, claset_of, clasimpset_of.
2009-07-23 wenzelm 2009-07-23 local simpset_of;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-23 wenzelm 2009-07-23 merged
2009-07-23 wenzelm 2009-07-23 paramify_vars: Term_Subst.map_atypsT_same recovered coding conventions of this module;
2009-07-23 wenzelm 2009-07-23 clarified pretty_goals, pretty_thm_aux: plain context; explicit pretty_goals_without_context, print_goals_without_context; tuned;
2009-07-23 wenzelm 2009-07-23 use regular Display.string_of_thm_global;
2009-07-23 wenzelm 2009-07-23 tuned ML_OPTIONS;
2009-07-23 haftmann 2009-07-23 fixed doc
2009-07-23 berghofe 2009-07-23 Purely functional type inference.
2009-07-22 haftmann 2009-07-22 merged
2009-07-22 haftmann 2009-07-22 moved complete_lattice &c. into separate theory
2009-07-22 Christian Urban 2009-07-22 merged
2009-07-22 Christian Urban 2009-07-22 tuned proofs and added some lemmas
2009-07-22 haftmann 2009-07-22 merged
2009-07-22 haftmann 2009-07-22 set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
2009-07-22 haftmann 2009-07-22 set intersection and union now named inter and union
2009-07-22 haftmann 2009-07-22 spurious proof failure
2009-07-22 wenzelm 2009-07-22 original rail implementation by Michael Kerscher;
2009-07-22 wenzelm 2009-07-22 merged, resolving trivial conflict;
2009-07-22 nipkow 2009-07-22 News
2009-07-22 haftmann 2009-07-22 explicit antiquotation
2009-07-21 haftmann 2009-07-21 merged
2009-07-21 haftmann 2009-07-21 merged
2009-07-21 haftmann 2009-07-21 obey captialized directory names convention
2009-07-21 haftmann 2009-07-21 dropped ancient flat_names option
2009-07-21 haftmann 2009-07-21 dropped ancient flat_names option
2009-07-21 haftmann 2009-07-21 integrated add_triv_classes into evaluation stack
2009-07-21 haftmann 2009-07-21 more accurate check of judgment type
2009-07-21 haftmann 2009-07-21 UNIV_code now named UNIV_apply
2009-07-21 haftmann 2009-07-21 attempt for more concise setup of non-etacontracting binders
2009-07-21 haftmann 2009-07-21 moved abstract algebra section to the end
2009-07-21 haftmann 2009-07-21 merged
2009-07-21 haftmann 2009-07-21 Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
2009-07-21 haftmann 2009-07-21 merged
2009-07-21 haftmann 2009-07-21 swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
2009-07-20 haftmann 2009-07-20 merged