| 2007-05-09 |
huffman |
add lemma hnorm_hyperpow
|
changeset |
files
|
| 2007-05-09 |
huffman |
add lemma of_hypreal_hyperpow
|
changeset |
files
|
| 2007-05-09 |
haftmann |
tuned
|
changeset |
files
|
| 2007-05-09 |
haftmann |
moved recfun_codegen.ML to Code_Generator.thy
|
changeset |
files
|
| 2007-05-09 |
haftmann |
continued
|
changeset |
files
|
| 2007-05-08 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| 2007-05-08 |
huffman |
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
|
changeset |
files
|
| 2007-05-08 |
huffman |
add lemma hnorm_divide
|
changeset |
files
|
| 2007-05-08 |
huffman |
add lemmas abs_hnorm_cancel, hnorm_of_hypreal
|
changeset |
files
|
| 2007-05-08 |
huffman |
add lemmas norm_add_less, norm_mult_less
|
changeset |
files
|
| 2007-05-08 |
huffman |
add lemma Standard_hyperpow
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
tuned;
|
changeset |
files
|
| 2007-05-08 |
huffman |
add of_hypreal constant with lemmas
|
changeset |
files
|
| 2007-05-08 |
huffman |
add lemmas norm_number_of, norm_of_int, norm_of_nat
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
quoted 'declaration';
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
simplified pretty_thm(_legacy);
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
is_sid: include '::';
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
tuned ProofDisplay.pretty_full_theory;
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
tuned;
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
updated;
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
simplified context data;
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
tuned;
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
legacy_intern_skolem: legacy_feature;
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
tuned;
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
renamed call_atp to sledgehammer;
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
updated;
|
changeset |
files
|
| 2007-05-08 |
wenzelm |
tuned context data;
|
changeset |
files
|
| 2007-05-08 |
haftmann |
ML adaptions
|
changeset |
files
|
| 2007-05-08 |
huffman |
clean up complex norm proofs, remove redundant lemmas
|
changeset |
files
|
| 2007-05-08 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| 2007-05-08 |
huffman |
fix proof of hypreal_sqrt_sum_squares_ge1
|
changeset |
files
|
| 2007-05-08 |
huffman |
add lemma real_sqrt_sum_squares_triangle_ineq
|
changeset |
files
|
| 2007-05-08 |
huffman |
add lemma abs_norm_cancel
|
changeset |
files
|
| 2007-05-08 |
huffman |
cleaned up
|
changeset |
files
|
| 2007-05-07 |
urbanc |
polished some proofs
|
changeset |
files
|
| 2007-05-07 |
huffman |
add lemmas power2_le_imp_le and power2_less_imp_less
|
changeset |
files
|
| 2007-05-07 |
huffman |
add lemma power_less_imp_less_base
|
changeset |
files
|
| 2007-05-07 |
huffman |
clean up RealVector classes
|
changeset |
files
|
| 2007-05-07 |
paulson |
First-order variant of the fully-typed translation
|
changeset |
files
|
| 2007-05-07 |
haftmann |
added further equality example
|
changeset |
files
|
| 2007-05-07 |
haftmann |
changed 'code nofunc' to 'code func del'
|
changeset |
files
|
| 2007-05-06 |
wenzelm |
* Context data interfaces;
|
changeset |
files
|
| 2007-05-06 |
wenzelm |
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
|
changeset |
files
|
| 2007-05-06 |
wenzelm |
simplified DataFun interfaces;
|
changeset |
files
|
| 2007-05-06 |
haftmann |
changed code generator invocation syntax
|
changeset |
files
|
| 2007-05-06 |
haftmann |
PreList imports RecDef
|
changeset |
files
|
| 2007-05-06 |
haftmann |
dropped legacy ML binding
|
changeset |
files
|
| 2007-05-06 |
haftmann |
added auxiliary lemmas for proof tools
|
changeset |
files
|
| 2007-05-06 |
haftmann |
dropped preorders, unified syntax
|
changeset |
files
|
| 2007-05-06 |
haftmann |
minimal import
|
changeset |
files
|
| 2007-05-06 |
haftmann |
dropped HOL.ML
|
changeset |
files
|
| 2007-05-06 |
haftmann |
tuned
|
changeset |
files
|
| 2007-05-06 |
wenzelm |
updated Alice version;
|
changeset |
files
|
| 2007-05-06 |
wenzelm |
IntInf.fromInt;
|
changeset |
files
|
| 2007-05-06 |
nipkow |
added "set" supression
|
changeset |
files
|
| 2007-05-06 |
nipkow |
added test about "set" supression
|
changeset |
files
|
| 2007-05-04 |
urbanc |
polished all proofs and made the theory "self-contained"
|
changeset |
files
|
| 2007-05-03 |
urbanc |
deleted some unnecessary type-annotations
|
changeset |
files
|
| 2007-05-03 |
urbanc |
tuned some of the proofs and added the lemma fresh_bool
|
changeset |
files
|
| 2007-05-02 |
nipkow |
tuned allpairs
|
changeset |
files
|