| 2006-09-21 |
huffman |
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
|
changeset |
files
|
| 2006-09-20 |
isatest |
choose gnuplot terminal by platform
|
changeset |
files
|
| 2006-09-20 |
wenzelm |
set terminal png color -- works for older versions of gnuplot;
|
changeset |
files
|
| 2006-09-20 |
wenzelm |
added ZF-UNITY;
|
changeset |
files
|
| 2006-09-20 |
paulson |
tidied
|
changeset |
files
|
| 2006-09-20 |
mengj |
Added in combinator reduction axioms for B' C' and S'. Also split the original reduction axioms into separate files: I+K, B+C, S, B'+C', S'.
|
changeset |
files
|
| 2006-09-20 |
isatest |
make it work on sunbroy2
|
changeset |
files
|
| 2006-09-20 |
mengj |
Moved the functional equality axioms to helper1 files.
|
changeset |
files
|
| 2006-09-20 |
mengj |
Introduced combinators B', C' and S'.
|
changeset |
files
|
| 2006-09-20 |
mengj |
Removed include_min_comb and include_combS.
|
changeset |
files
|
| 2006-09-20 |
aspinall |
Add Source.of_instream_slurp to try to ensure that XML parser sees whole documents.
|
changeset |
files
|
| 2006-09-20 |
haftmann |
improvements for codegen 2
|
changeset |
files
|
| 2006-09-20 |
haftmann |
name shifts
|
changeset |
files
|
| 2006-09-20 |
haftmann |
fixed bug
|
changeset |
files
|
| 2006-09-20 |
krauss |
Removed "induct set" attribute from total induction rules
|
changeset |
files
|
| 2006-09-20 |
haftmann |
removed debug
|
changeset |
files
|
| 2006-09-20 |
krauss |
Fixed error in pattern splitting algorithm
|
changeset |
files
|
| 2006-09-20 |
huffman |
change section to subsection
|
changeset |
files
|
| 2006-09-20 |
huffman |
add header
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
renamed axclass_xxxx axclasses;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
tuned;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
added standard;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
added name_classrel/arities/arity;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
pretty_full_theory: suppress internal entities by default;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
Logic.name_classrel/arities;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
revert to previous version;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
added General/susp.ML;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
removed duplicate arities;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
sko/abs: Name.internal prevents choking of print_theory;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
tuned method setup;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
'print_theory': bang option for full verbosity;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
* Pure: 'print_theory' now suppresses entities with internal name;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
tuned;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
simple html output;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
timespan: 100 days;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
superceded by isatest-statistics;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
tuned;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
target dir;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
Standard statistics.
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
time: include year;
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
Produce statistics from isatest session logs.
|
changeset |
files
|
| 2006-09-19 |
wenzelm |
moved Import/susp.ML to Pure/General;
|
changeset |
files
|
| 2006-09-19 |
obua |
renamed axclass_xxxx axclasses
|
changeset |
files
|
| 2006-09-19 |
haftmann |
removed diagnostic messages
|
changeset |
files
|
| 2006-09-19 |
haftmann |
Operational Equality
|
changeset |
files
|
| 2006-09-19 |
urbanc |
this file contains a compile-challenge suggested by Adam Chlipala;
|
changeset |
files
|
| 2006-09-19 |
urbanc |
tuned
|
changeset |
files
|
| 2006-09-19 |
haftmann |
added auxiliary lemma for code generation 2
|
changeset |
files
|
| 2006-09-19 |
haftmann |
removed
|
changeset |
files
|
| 2006-09-19 |
haftmann |
moved part of normalization oracle here
|
changeset |
files
|
| 2006-09-19 |
haftmann |
classical arity syntax
|
changeset |
files
|
| 2006-09-19 |
haftmann |
added codegen_data
|
changeset |
files
|
| 2006-09-19 |
haftmann |
moved base setup for evaluation oracle hier
|
changeset |
files
|
| 2006-09-19 |
haftmann |
added OperationalEquality.thy
|
changeset |
files
|
| 2006-09-19 |
haftmann |
code generation 2 adjustments
|
changeset |
files
|
| 2006-09-19 |
haftmann |
(void)
|
changeset |
files
|
| 2006-09-19 |
haftmann |
improved numeral handling for nbe
|
changeset |
files
|
| 2006-09-19 |
haftmann |
added suspensions in Pure
|
changeset |
files
|
| 2006-09-19 |
haftmann |
added some stuff for code generation 2
|
changeset |
files
|