| Fri, 23 Jul 2010 14:07:35 +0200 |
blanchet |
fix polymorphic "val"
|
changeset |
files
|
| Sat, 24 Jul 2010 18:08:43 +0200 |
haftmann |
temporarily deactivating check for Scala
|
changeset |
files
|
| Sat, 24 Jul 2010 18:08:41 +0200 |
haftmann |
another refinement chapter in the neverending numeral story
|
changeset |
files
|
| Mon, 26 Jul 2010 17:59:26 +0200 |
wenzelm |
inductive_cases: crude parallelization via Par_List.map;
|
changeset |
files
|
| Mon, 26 Jul 2010 17:41:26 +0200 |
wenzelm |
modernized/unified some specifications;
|
changeset |
files
|
| Mon, 26 Jul 2010 13:50:52 +0200 |
wenzelm |
Thy_Info.loaded_files: Thy_Load.loaded_files depends on master -- i.e. no files for finished theory;
|
changeset |
files
|
| Sun, 25 Jul 2010 21:42:39 +0200 |
wenzelm |
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
|
changeset |
files
|
| Sun, 25 Jul 2010 14:41:48 +0200 |
wenzelm |
simplified handling of theory begin/end wrt. toplevel and theory loader;
|
changeset |
files
|
| Sun, 25 Jul 2010 12:57:29 +0200 |
wenzelm |
Thy_Load.check_loaded via Theory.at_end;
|
changeset |
files
|
| Sat, 24 Jul 2010 21:40:48 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 24 Jul 2010 21:22:21 +0200 |
wenzelm |
moved basic thy file name operations from Thy_Load to Thy_Header;
|
changeset |
files
|
| Sat, 24 Jul 2010 12:14:53 +0200 |
wenzelm |
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
|
changeset |
files
|
| Fri, 23 Jul 2010 18:42:46 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 23 Jul 2010 10:58:13 +0200 |
haftmann |
avoid unreliable Haskell Int type
|
changeset |
files
|
| 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
|