| Fri, 23 Jul 2010 10:25:00 +0200 |
haftmann |
proper subclass instead of sublocale
|
changeset |
files
|
| Fri, 23 Jul 2010 09:05:54 +0200 |
haftmann |
repaired tool invocation
|
changeset |
files
|
| Fri, 23 Jul 2010 18:42:35 +0200 |
wenzelm |
observe standard conventions for doc-strings;
|
changeset |
files
|
| Thu, 22 Jul 2010 23:29:39 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Thu, 22 Jul 2010 22:58:18 +0200 |
wenzelm |
eliminated some unused Thy_Info operations;
|
changeset |
files
|
| Thu, 22 Jul 2010 22:50:35 +0200 |
wenzelm |
refrain from generating <hr/> and from "hiding" it in isabelle.css -- the latter might be used in other situations as well;
|
changeset |
files
|
| Thu, 22 Jul 2010 22:39:31 +0200 |
wenzelm |
generic external source files -- nothing special about ML here;
|
changeset |
files
|
| Thu, 22 Jul 2010 22:31:20 +0200 |
wenzelm |
discontinued special treatment of ML files -- no longer complete extensions on demand;
|
changeset |
files
|
| Thu, 22 Jul 2010 20:46:45 +0200 |
wenzelm |
eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL;
|
changeset |
files
|
| Thu, 22 Jul 2010 20:36:41 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 22 Jul 2010 18:08:39 +0200 |
wenzelm |
updated some headers;
|
changeset |
files
|
| Thu, 22 Jul 2010 17:26:31 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 22 Jul 2010 17:26:22 +0200 |
haftmann |
dedicated exec ... syntax for open state monad (partly already introduces in d00a3f47b607)
|
changeset |
files
|
| Thu, 22 Jul 2010 16:53:00 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 22 Jul 2010 12:07:30 +0200 |
haftmann |
more generous memory settings for scala check
|
changeset |
files
|
| Thu, 22 Jul 2010 11:29:31 +0200 |
blanchet |
no polymorphic "var"s
|
changeset |
files
|
| Thu, 22 Jul 2010 08:37:46 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Wed, 21 Jul 2010 19:21:07 +0200 |
bulwahn |
adding checking of expected result for the tool quickcheck; annotated a few quickcheck examples
|
changeset |
files
|
| Wed, 21 Jul 2010 21:16:58 +0200 |
blanchet |
do a better job at Skolemizing in Nitpick, for TPTP FOF
|
changeset |
files
|
| Wed, 21 Jul 2010 21:15:49 +0200 |
blanchet |
revert code that was submitted by mistake
|
changeset |
files
|
| Wed, 21 Jul 2010 21:15:07 +0200 |
blanchet |
renamings + only need second component of name pool to reconstruct proofs
|
changeset |
files
|
| Wed, 21 Jul 2010 21:14:47 +0200 |
blanchet |
rename "classrel" to "class_rel"
|
changeset |
files
|
| Wed, 21 Jul 2010 21:14:26 +0200 |
blanchet |
rename "combtyp" constructors
|
changeset |
files
|
| Wed, 21 Jul 2010 21:14:07 +0200 |
blanchet |
renamed "Literal" to "FOLLiteral"
|
changeset |
files
|
| Wed, 21 Jul 2010 21:13:46 +0200 |
blanchet |
renamed "HOLClause" to "FOLClause" -- it's really a FOL clause with combinators
|
changeset |
files
|
| Wed, 21 Jul 2010 18:13:15 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
fixing quickcheck invocation in HOL-Mirabelle
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
hiding constants in Quickcheck_Types
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
adding a type for flat complete lattice to Quickcheck_Types
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
added new theories to IsaMakefile and ROOT.ML
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
adding Quickcheck examples for other quickcheck default types
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
adding Library theory for other quickcheck default types
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
removing obsolete ID in Quickcheck_Examples
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
correcting wellsortedness check and improving error message
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
using multiple default types in quickcheck
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
correcting merging of default_types
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
reordering quickcheck signature; exporting test_params and inspection function
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
changed default types to a list of types; extended quickcheck parameters to be a list of values to parse a list of default types
|
changeset |
files
|
| Wed, 21 Jul 2010 18:11:51 +0200 |
bulwahn |
putting proof in the right context; adding if rewriting; tuned
|
changeset |
files
|
| Thu, 22 Jul 2010 16:43:21 +0200 |
wenzelm |
load_thy: parallel parsing of units, which consist of statement/proof each;
|
changeset |
files
|
| Thu, 22 Jul 2010 14:59:27 +0200 |
wenzelm |
eliminated some unreferenced identifiers;
|
changeset |
files
|
| Thu, 22 Jul 2010 14:01:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 22 Jul 2010 10:41:12 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Wed, 21 Jul 2010 21:08:40 +0200 |
wenzelm |
replaced Source.of_list_limited by slightly more economic Source.of_string_limited;
|
changeset |
files
|
| Wed, 21 Jul 2010 20:32:08 +0200 |
wenzelm |
deps_thy/load_thy: store compact text to reduce space by factor 12;
|
changeset |
files
|
| Wed, 21 Jul 2010 17:57:16 +0200 |
wenzelm |
make SML/NJ happy, by adhoc type-constraints;
|
changeset |
files
|
| Wed, 21 Jul 2010 17:55:07 +0200 |
wenzelm |
recovered benchmarks, which are not tested automatically;
|
changeset |
files
|
| Wed, 21 Jul 2010 17:46:36 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Wed, 21 Jul 2010 16:50:42 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 21 Jul 2010 09:46:36 +0200 |
haftmann |
abstract visualization of locale ingredients; all_locales yields proper locale identifiers
|
changeset |
files
|
| Tue, 20 Jul 2010 14:08:47 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Tue, 20 Jul 2010 14:01:06 +0200 |
haftmann |
accomodate for scope of "as" binding in ML
|
changeset |
files
|
| Tue, 20 Jul 2010 10:24:18 +0200 |
haftmann |
tuned code
|
changeset |
files
|
| Tue, 20 Jul 2010 08:54:21 +0200 |
haftmann |
datatype classes are abstract
|
changeset |
files
|
| Tue, 20 Jul 2010 08:54:21 +0200 |
haftmann |
avoid deprecation
|
changeset |
files
|
| Tue, 20 Jul 2010 06:35:29 +0200 |
haftmann |
robustified metis proof
|
changeset |
files
|
| Mon, 19 Jul 2010 20:23:52 +0200 |
haftmann |
modernized abel_cancel simproc setup
|
changeset |
files
|
| Mon, 19 Jul 2010 20:23:49 +0200 |
haftmann |
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
|
changeset |
files
|
| Mon, 19 Jul 2010 20:19:03 +0200 |
haftmann |
diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq
|
changeset |
files
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
changeset |
files
|