| 2009-11-10 |
wenzelm |
removed obsolete name_of -- cf. decode;
|
changeset |
files
|
| 2009-11-10 |
wenzelm |
desymbolize: use Symbol.decode directly;
|
changeset |
files
|
| 2009-11-10 |
wenzelm |
try SAT_Examples last, to minimize impact of global side-effects;
|
changeset |
files
|
| 2009-11-10 |
wenzelm |
home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
|
changeset |
files
|
| 2009-11-10 |
paulson |
Inserted missing theory dependency
|
changeset |
files
|
| 2009-11-09 |
wenzelm |
merged
|
changeset |
files
|
| 2009-11-09 |
ballarin |
Merged.
|
changeset |
files
|
| 2009-11-09 |
ballarin |
Removed obsolete code.
|
changeset |
files
|
| 2009-11-09 |
wenzelm |
updated to official Poly/ML 5.3.0;
|
changeset |
files
|
| 2009-11-09 |
wenzelm |
switched some isatest sessions to official Poly/ML 5.3.0;
|
changeset |
files
|
| 2009-11-09 |
wenzelm |
setup for official Poly/ML 5.3.0, which is now the default;
|
changeset |
files
|
| 2009-11-09 |
wenzelm |
locale_const/target_notation: uniform use of Term.aconv_untyped;
|
changeset |
files
|
| 2009-11-09 |
wenzelm |
eliminated hard tabulators;
|
changeset |
files
|
| 2009-11-09 |
paulson |
fixed some inappropriate names
|
changeset |
files
|
| 2009-11-09 |
paulson |
merged
|
changeset |
files
|
| 2009-11-09 |
paulson |
New theory Probability/Borel.thy, and some associated lemmas
|
changeset |
files
|
| 2009-11-09 |
haftmann |
merged
|
changeset |
files
|
| 2009-11-09 |
haftmann |
tuned error messages; tuned code
|
changeset |
files
|
| 2009-11-09 |
boehmes |
follow standard theory merge behaviour: do not change already selected solver
|
changeset |
files
|
| 2009-11-09 |
boehmes |
generalized proof by abstraction,
|
changeset |
files
|
| 2009-11-09 |
boehmes |
made theory merge deterministic wrt. the selected solver
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
merged
|
changeset |
files
|
| 2009-11-08 |
berghofe |
merged
|
changeset |
files
|
| 2009-11-08 |
berghofe |
Repaired handling of comprehensions in "values" command.
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
updated functor Theory_Data, Proof_Data, Generic_Data;
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
modernized structure Reorient_Proc;
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
adapted Theory_Data;
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
adapted Theory_Data;
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
tuned;
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
adapted Generic_Data;
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
added "declaration (pervasive)";
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
print_theorems: suppress concealed (global) facts, unless "!" option is given;
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
updated generated file;
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
modernized structure Random_Word;
|
changeset |
files
|
| 2009-11-08 |
wenzelm |
init_component: slightly more robust read (raw input, succeed on non-terminated last line);
|
changeset |
files
|
| 2009-11-07 |
webertj |
merged
|
changeset |
files
|
| 2009-11-07 |
webertj |
Due to popular demand: added a function that benchmarks proof reconstruction
|
changeset |
files
|
| 2009-11-07 |
webertj |
Turned sections into subsections (better document structure).
|
changeset |
files
|
| 2009-11-07 |
huffman |
merged
|
changeset |
files
|
| 2009-11-07 |
huffman |
merged
|
changeset |
files
|
| 2009-11-06 |
huffman |
fix name of lemma snd_strict
|
changeset |
files
|
| 2009-11-05 |
huffman |
use try instead of handle
|
changeset |
files
|
| 2009-11-05 |
huffman |
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
|
changeset |
files
|
| 2009-11-05 |
huffman |
lemma deflation_strict
|
changeset |
files
|
| 2009-11-07 |
wenzelm |
tuned ML_OPTIONS for SML/NJ -- for improved performance;
|
changeset |
files
|
| 2009-11-07 |
haftmann |
merged
|
changeset |
files
|
| 2009-11-07 |
haftmann |
added predicate example
|
changeset |
files
|
| 2009-11-07 |
haftmann |
tuned
|
changeset |
files
|
| 2009-11-07 |
haftmann |
modernized primrec
|
changeset |
files
|
| 2009-11-06 |
boehmes |
made SML/NJ happy
|
changeset |
files
|
| 2009-11-06 |
nipkow |
merged
|
changeset |
files
|
| 2009-11-04 |
nipkow |
merged
|
changeset |
files
|
| 2009-10-29 |
nipkow |
Replaced exception CRing by error because it is meant for the user.
|
changeset |
files
|
| 2009-11-06 |
nipkow |
merged
|
changeset |
files
|
| 2009-11-06 |
nipkow |
Command atp_minimize uses the naive linear algorithm now
|
changeset |
files
|
| 2009-11-06 |
bulwahn |
merged
|
changeset |
files
|
| 2009-11-06 |
bulwahn |
merged
|
changeset |
files
|
| 2009-11-06 |
bulwahn |
merged
|
changeset |
files
|