| Tue, 27 Jul 2010 23:15:37 +0200 |
wenzelm |
clarified register_thy: clean slate via kill_thy, more precise CRITICAL section;
|
changeset |
files
|
| Tue, 27 Jul 2010 23:04:50 +0200 |
wenzelm |
updated keywords;
|
changeset |
files
|
| Tue, 27 Jul 2010 23:02:45 +0200 |
wenzelm |
updated manual concerning theory loader;
|
changeset |
files
|
| Tue, 27 Jul 2010 23:01:42 +0200 |
wenzelm |
theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
|
changeset |
files
|
| Tue, 27 Jul 2010 22:42:53 +0200 |
wenzelm |
avoid repeated File.read for theory text (as before);
|
changeset |
files
|
| Tue, 27 Jul 2010 22:23:32 +0200 |
wenzelm |
tuned messages and comments;
|
changeset |
files
|
| Tue, 27 Jul 2010 22:15:51 +0200 |
wenzelm |
simplified Thy_Header.read -- include Source.of_string_limited here;
|
changeset |
files
|
| Tue, 27 Jul 2010 22:00:26 +0200 |
wenzelm |
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
|
changeset |
files
|
| Tue, 27 Jul 2010 12:59:22 +0200 |
wenzelm |
more precise stats;
|
changeset |
files
|
| Mon, 26 Jul 2010 18:25:19 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 26 Jul 2010 14:44:07 +0200 |
haftmann |
quickcheck images of goals under registration morphisms
|
changeset |
files
|
| Mon, 26 Jul 2010 14:44:07 +0200 |
haftmann |
get_registrations interface
|
changeset |
files
|
| Mon, 26 Jul 2010 11:15:10 +0200 |
haftmann |
restored unusual snd-biased merge/join policy -- required due to non-conservative code setups
|
changeset |
files
|
| 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
|