2007-05-08 wenzelm 2007-05-08 tuned;
2007-05-08 huffman 2007-05-08 add of_hypreal constant with lemmas
2007-05-08 huffman 2007-05-08 add lemmas norm_number_of, norm_of_int, norm_of_nat
2007-05-08 wenzelm 2007-05-08 quoted 'declaration';
2007-05-08 wenzelm 2007-05-08 simplified pretty_thm(_legacy);
2007-05-08 wenzelm 2007-05-08 is_sid: include '::';
2007-05-08 wenzelm 2007-05-08 tuned ProofDisplay.pretty_full_theory;
2007-05-08 wenzelm 2007-05-08 tuned;
2007-05-08 wenzelm 2007-05-08 updated;
2007-05-08 wenzelm 2007-05-08 simplified context data;
2007-05-08 wenzelm 2007-05-08 tuned;
2007-05-08 wenzelm 2007-05-08 legacy_intern_skolem: legacy_feature;
2007-05-08 wenzelm 2007-05-08 tuned;
2007-05-08 wenzelm 2007-05-08 renamed call_atp to sledgehammer;
2007-05-08 wenzelm 2007-05-08 updated;
2007-05-08 wenzelm 2007-05-08 tuned context data;
2007-05-08 haftmann 2007-05-08 ML adaptions
2007-05-08 huffman 2007-05-08 clean up complex norm proofs, remove redundant lemmas
2007-05-08 huffman 2007-05-08 remove redundant lemmas
2007-05-08 huffman 2007-05-08 fix proof of hypreal_sqrt_sum_squares_ge1
2007-05-08 huffman 2007-05-08 add lemma real_sqrt_sum_squares_triangle_ineq
2007-05-08 huffman 2007-05-08 add lemma abs_norm_cancel
2007-05-08 huffman 2007-05-08 cleaned up
2007-05-08 urbanc 2007-05-08 polished some proofs
2007-05-08 huffman 2007-05-08 add lemmas power2_le_imp_le and power2_less_imp_less
2007-05-08 huffman 2007-05-08 add lemma power_less_imp_less_base
2007-05-07 huffman 2007-05-07 clean up RealVector classes
2007-05-07 paulson 2007-05-07 First-order variant of the fully-typed translation
2007-05-07 haftmann 2007-05-07 added further equality example
2007-05-07 haftmann 2007-05-07 changed 'code nofunc' to 'code func del'
2007-05-07 wenzelm 2007-05-07 * Context data interfaces;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-05-06 haftmann 2007-05-06 PreList imports RecDef
2007-05-06 haftmann 2007-05-06 dropped legacy ML binding
2007-05-06 haftmann 2007-05-06 added auxiliary lemmas for proof tools
2007-05-06 haftmann 2007-05-06 dropped preorders, unified syntax
2007-05-06 haftmann 2007-05-06 minimal import
2007-05-06 haftmann 2007-05-06 dropped HOL.ML
2007-05-06 haftmann 2007-05-06 tuned
2007-05-06 wenzelm 2007-05-06 updated Alice version;
2007-05-06 wenzelm 2007-05-06 IntInf.fromInt;
2007-05-06 nipkow 2007-05-06 added "set" supression
2007-05-06 nipkow 2007-05-06 added test about "set" supression
2007-05-04 urbanc 2007-05-04 polished all proofs and made the theory "self-contained"
2007-05-03 urbanc 2007-05-03 deleted some unnecessary type-annotations
2007-05-03 urbanc 2007-05-03 tuned some of the proofs and added the lemma fresh_bool
2007-05-02 nipkow 2007-05-02 tuned allpairs
2007-05-02 urbanc 2007-05-02 tuned some proofs and changed variable names in some definitions of Nominal.thy
2007-04-30 nipkow 2007-04-30 added allpairs
2007-04-30 wenzelm 2007-04-30 removed obsolete get_sg;
2007-04-30 wenzelm 2007-04-30 explicit treatment of legacy_features;
2007-04-30 paulson 2007-04-30 Fixing bugs in the partial-typed and fully-typed translations
2007-04-30 paulson 2007-04-30 Removal of dead code
2007-04-27 urbanc 2007-04-27 tuned some proofs in CR and properly included CR_Takahashi
2007-04-27 wenzelm 2007-04-27 removed obsolete induct/simp tactic;
2007-04-27 urbanc 2007-04-27 alternative and much simpler proof for Church-Rosser of Beta-Reduction
2007-04-27 kleing 2007-04-27 use correct email program for sunbroy2
2007-04-26 wenzelm 2007-04-26 removed legacy ML files;