2013-03-26 |
wenzelm |
tuned session specification;
|
file |
diff |
annotate
|
2013-02-15 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
2012-10-19 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
2012-09-13 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
2012-04-20 |
hoelzl |
hide code generation facts in the Float theory, they are only exported for Approximation
|
file |
diff |
annotate
|
2012-04-19 |
hoelzl |
use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
|
file |
diff |
annotate
|
2012-04-18 |
hoelzl |
use lifting to introduce floating point numbers
|
file |
diff |
annotate
|
2012-04-18 |
hoelzl |
replace the float datatype by a type with unique representation
|
file |
diff |
annotate
|
2012-03-25 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
2012-02-12 |
haftmann |
tuned
|
file |
diff |
annotate
|
2011-11-13 |
huffman |
remove lemma float_remove_real_numeral, which duplicated Float.float_number_of
|
file |
diff |
annotate
|
2011-10-12 |
wenzelm |
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
|
file |
diff |
annotate
|
2011-09-07 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
2011-08-28 |
huffman |
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
|
file |
diff |
annotate
|
2011-08-20 |
huffman |
remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
|
file |
diff |
annotate
|
2011-08-19 |
huffman |
fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
|
file |
diff |
annotate
|
2011-08-19 |
huffman |
remove some redundant simp rules
|
file |
diff |
annotate
|
2011-04-16 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
2010-12-29 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
2010-12-06 |
hoelzl |
move coercions to appropriate places
|
file |
diff |
annotate
|
2010-12-06 |
nipkow |
moved coercion decl. for int
|
file |
diff |
annotate
|
2010-12-02 |
wenzelm |
proper theory name (cf. e84f82418e09);
|
file |
diff |
annotate
|
2010-12-02 |
hoelzl |
Use coercions in Approximation (by Dmitriy Traytel).
|
file |
diff |
annotate
|
2010-09-20 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
2010-08-28 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
2010-08-26 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
2010-08-25 |
wenzelm |
approximation_oracle: actually match true/false in ML, not arbitrary values;
|
file |
diff |
annotate
|
2010-08-19 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
2010-08-19 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
2010-07-19 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
2010-07-01 |
haftmann |
qualified constants Set.member and Set.Collect
|
file |
diff |
annotate
|
2010-06-14 |
haftmann |
removed simplifier congruence rule of "prod_case"
|
file |
diff |
annotate
|
2010-06-10 |
haftmann |
tuned quotes, antiquotations and whitespace
|
file |
diff |
annotate
|
2010-05-19 |
haftmann |
spelt out normalizer explicitly -- avoid dynamic reference to code generator configuration; avoid using old Codegen.eval_term
|
file |
diff |
annotate
|
2010-05-17 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
2010-05-10 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
2010-04-29 |
haftmann |
code_reflect: specify module name directly after keyword
|
file |
diff |
annotate
|
2010-04-28 |
haftmann |
use code_reflect
|
file |
diff |
annotate
|
2010-03-20 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
2010-02-23 |
huffman |
adapt to new realpow rules
|
file |
diff |
annotate
|
2010-02-10 |
haftmann |
rely less on ordered rewriting
|
file |
diff |
annotate
|
2010-02-05 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
2009-10-20 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2009-10-17 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
2009-10-13 |
hoelzl |
order conjunctions to be printed without parentheses
|
file |
diff |
annotate
|
2009-10-13 |
hoelzl |
approximation now fails earlier when using interval splitting; value [approximate] now supports bounded variables; renamed Var -> Atom for better readability
|
file |
diff |
annotate
|
2009-09-23 |
hoelzl |
correct variable order in approximate-method
|
file |
diff |
annotate
|
2009-09-22 |
haftmann |
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
|
file |
diff |
annotate
|
2009-08-28 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|
2009-07-30 |
wenzelm |
qualified Subgoal.FOCUS;
|
file |
diff |
annotate
|
2009-07-26 |
wenzelm |
replaced old METAHYPS by FOCUS;
|
file |
diff |
annotate
|
2009-06-30 |
hoelzl |
use DERIV_intros
|
file |
diff |
annotate
|
2009-06-29 |
hoelzl |
Implemented taylor series expansion for approximation
|
file |
diff |
annotate
|
2009-06-25 |
hoelzl |
Improved computation of bounds and implemented interval splitting for 'approximation'.
|
file |
diff |
annotate
|
2009-06-08 |
hoelzl |
Added new evaluator "approximate"
|
file |
diff |
annotate
|
2009-06-15 |
hoelzl |
tuned
|
file |
diff |
annotate
|
2009-06-24 |
nipkow |
corrected and unified thm names
|
file |
diff |
annotate
|
2009-06-08 |
hoelzl |
Better approximation of cos around pi.
|
file |
diff |
annotate
|
2009-06-05 |
hoelzl |
Approximation: Corrected precision of ln on all real values
|
file |
diff |
annotate
|
2009-06-04 |
hoelzl |
Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
|
file |
diff |
annotate
|