| Mon, 26 Jul 2010 11:11:10 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 26 Jul 2010 11:10:57 +0200 |
haftmann |
reactivated Scala check
|
changeset |
files
|
| Mon, 26 Jul 2010 11:10:36 +0200 |
haftmann |
corrected range check once more
|
changeset |
files
|
| Mon, 26 Jul 2010 11:10:35 +0200 |
haftmann |
added Code_Natural.thy
|
changeset |
files
|
| Mon, 26 Jul 2010 11:09:45 +0200 |
haftmann |
reactivated Scala check; tuned import order
|
changeset |
files
|
| Mon, 26 Jul 2010 11:09:45 +0200 |
haftmann |
reactivated Scala check
|
changeset |
files
|
| Mon, 26 Jul 2010 11:09:44 +0200 |
haftmann |
modified namespace policy
|
changeset |
files
|
| Mon, 26 Jul 2010 11:09:44 +0200 |
haftmann |
use Natural as index type for Haskell and Scala
|
changeset |
files
|
| Sun, 25 Jul 2010 15:43:53 +0200 |
blanchet |
merged
|
changeset |
files
|
| Fri, 23 Jul 2010 21:29:29 +0200 |
blanchet |
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
|
changeset |
files
|
| Fri, 23 Jul 2010 15:04:49 +0200 |
blanchet |
first step in using "fof" rather than "cnf" in TPTP problems
|
changeset |
files
|
| 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
|