| Thu, 29 Jul 2010 09:41:49 +0200 |
blanchet |
improved ATP error handling some more
|
changeset |
files
|
| Thu, 29 Jul 2010 00:28:57 +0200 |
blanchet |
shorter URL
|
changeset |
files
|
| Wed, 28 Jul 2010 23:44:18 +0200 |
blanchet |
mention version numbers
|
changeset |
files
|
| Wed, 28 Jul 2010 23:05:35 +0200 |
blanchet |
fiddled with usage text
|
changeset |
files
|
| Wed, 28 Jul 2010 23:01:27 +0200 |
blanchet |
handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
|
changeset |
files
|
| Thu, 29 Jul 2010 09:57:10 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 29 Jul 2010 09:57:00 +0200 |
haftmann |
tuned printing of applications and let cascades
|
changeset |
files
|
| Thu, 29 Jul 2010 09:56:59 +0200 |
haftmann |
checking Scala_imp
|
changeset |
files
|
| Thu, 29 Jul 2010 09:56:59 +0200 |
haftmann |
proper unit type in transformed program
|
changeset |
files
|
| Thu, 29 Jul 2010 08:16:49 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 28 Jul 2010 14:11:48 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 28 Jul 2010 12:12:32 +0200 |
haftmann |
tuned; added pretty numerals for code generation
|
changeset |
files
|
| Wed, 28 Jul 2010 12:12:29 +0200 |
haftmann |
may use `int` in Isabelle runtime environment
|
changeset |
files
|
| Wed, 28 Jul 2010 14:09:56 +0200 |
haftmann |
dropped dead code
|
changeset |
files
|
| Wed, 28 Jul 2010 22:18:35 +0200 |
blanchet |
merged
|
changeset |
files
|
| Wed, 28 Jul 2010 19:42:11 +0200 |
blanchet |
make Mirabelle happy
|
changeset |
files
|
| Wed, 28 Jul 2010 19:23:56 +0200 |
blanchet |
renamed environment variable
|
changeset |
files
|
| Wed, 28 Jul 2010 19:07:34 +0200 |
blanchet |
updated component name
|
changeset |
files
|
| Wed, 28 Jul 2010 19:04:59 +0200 |
blanchet |
consequence of directory renaming
|
changeset |
files
|
| Wed, 28 Jul 2010 19:01:34 +0200 |
blanchet |
rename directory
|
changeset |
files
|
| Wed, 28 Jul 2010 19:01:07 +0200 |
blanchet |
minor refactoring
|
changeset |
files
|
| Wed, 28 Jul 2010 18:54:18 +0200 |
blanchet |
minor refactoring
|
changeset |
files
|
| Wed, 28 Jul 2010 18:45:18 +0200 |
blanchet |
updated Sledgehammer docs
|
changeset |
files
|
| Wed, 28 Jul 2010 18:35:15 +0200 |
blanchet |
remove needless "-x" option, now that (1) we can't handle remote SPASS anymore; and (2) we can a priori parse the SPASS syntax in "Sledgehammer_Proof_Reconstruct" anyway
|
changeset |
files
|
| Wed, 28 Jul 2010 18:32:54 +0200 |
blanchet |
remove "remote_spass" because there's no way to find out which clauses come from which facts + rename scripts
|
changeset |
files
|
| Wed, 28 Jul 2010 18:07:25 +0200 |
blanchet |
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
|
changeset |
files
|
| Wed, 28 Jul 2010 17:38:40 +0200 |
blanchet |
revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well;
|
changeset |
files
|
| Wed, 28 Jul 2010 16:54:12 +0200 |
blanchet |
more robust proof reconstruction
|
changeset |
files
|
| Wed, 28 Jul 2010 16:13:34 +0200 |
blanchet |
adapt to new (?) TPTP output
|
changeset |
files
|
| Wed, 28 Jul 2010 15:53:52 +0200 |
blanchet |
fix remote_vampire's proof reconstruction
|
changeset |
files
|
| Wed, 28 Jul 2010 15:34:10 +0200 |
blanchet |
fix proof reconstruction for latest Vampire
|
changeset |
files
|
| Wed, 28 Jul 2010 10:45:49 +0200 |
blanchet |
renaming
|
changeset |
files
|
| Wed, 28 Jul 2010 10:06:06 +0200 |
blanchet |
support latest version of Vampire (1.0) locally
|
changeset |
files
|
| Wed, 28 Jul 2010 00:53:24 +0200 |
blanchet |
improve detection of installed SPASS
|
changeset |
files
|
| Wed, 28 Jul 2010 11:42:48 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 27 Jul 2010 20:16:14 +0200 |
blanchet |
merge
|
changeset |
files
|
| Tue, 27 Jul 2010 20:16:03 +0200 |
blanchet |
compile
|
changeset |
files
|
| Tue, 27 Jul 2010 19:41:19 +0200 |
blanchet |
minor refactoring
|
changeset |
files
|
| Tue, 27 Jul 2010 19:17:15 +0200 |
blanchet |
standardize "Author" tags
|
changeset |
files
|
| Tue, 27 Jul 2010 18:50:22 +0200 |
blanchet |
remove unused fun
|
changeset |
files
|
| Tue, 27 Jul 2010 18:45:55 +0200 |
blanchet |
reorder ML files in theory
|
changeset |
files
|
| Tue, 27 Jul 2010 18:38:10 +0200 |
blanchet |
get rid of "FOLClause" (obsoleted by FOF-enabled "FOLFormula")
|
changeset |
files
|
| Tue, 27 Jul 2010 18:33:10 +0200 |
blanchet |
more refactoring
|
changeset |
files
|
| Tue, 27 Jul 2010 17:58:30 +0200 |
blanchet |
kill needless tracing
|
changeset |
files
|
| Tue, 27 Jul 2010 17:56:01 +0200 |
blanchet |
rename "ATP_Manager" ML module to "Sledgehammer";
|
changeset |
files
|
| Tue, 27 Jul 2010 17:49:16 +0200 |
blanchet |
rename
|
changeset |
files
|
| Tue, 27 Jul 2010 17:43:11 +0200 |
blanchet |
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
|
changeset |
files
|
| Tue, 27 Jul 2010 17:32:55 +0200 |
blanchet |
renamed file
|
changeset |
files
|
| Tue, 27 Jul 2010 17:32:10 +0200 |
blanchet |
move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
|
changeset |
files
|
| Tue, 27 Jul 2010 17:15:12 +0200 |
blanchet |
get rid of more dead wood
|
changeset |
files
|
| Tue, 27 Jul 2010 17:04:09 +0200 |
blanchet |
implemented "sublinear" minimization algorithm
|
changeset |
files
|
| Tue, 27 Jul 2010 15:28:23 +0200 |
blanchet |
extract sort constraints from FOFs properly;
|
changeset |
files
|
| Tue, 27 Jul 2010 17:10:27 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 27 Jul 2010 17:09:35 +0200 |
haftmann |
delete structure Basic_Record; avoid `record` in names in structure Record
|
changeset |
files
|
| Tue, 27 Jul 2010 14:12:35 +0200 |
blanchet |
no polymorphic "var"
|
changeset |
files
|
| Tue, 27 Jul 2010 14:02:15 +0200 |
blanchet |
merged
|
changeset |
files
|
| Tue, 27 Jul 2010 13:16:37 +0200 |
blanchet |
shrink the "max_new_relevant_facts_per_iter" fudge factors, now that we count formulas and not clauses
|
changeset |
files
|
| Tue, 27 Jul 2010 13:15:58 +0200 |
blanchet |
negate tfree conjecture
|
changeset |
files
|
| Tue, 27 Jul 2010 12:01:02 +0200 |
blanchet |
handle Vampire's equality proxy axiom correctly
|
changeset |
files
|
| Tue, 27 Jul 2010 00:08:05 +0200 |
blanchet |
simplify code
|
changeset |
files
|
| Mon, 26 Jul 2010 23:54:40 +0200 |
blanchet |
prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)
|
changeset |
files
|
| Mon, 26 Jul 2010 22:35:25 +0200 |
blanchet |
remove obsolete field in record
|
changeset |
files
|
| Mon, 26 Jul 2010 22:32:37 +0200 |
blanchet |
simplify code
|
changeset |
files
|
| Mon, 26 Jul 2010 22:22:23 +0200 |
blanchet |
get rid of obsolete "axiom ID" component, since it's now always 0
|
changeset |
files
|
| Mon, 26 Jul 2010 20:07:31 +0200 |
blanchet |
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
|
changeset |
files
|
| Mon, 26 Jul 2010 17:56:10 +0200 |
blanchet |
added extensionalization to Sledgehammer, mimicking what the Clausifier used to do
|
changeset |
files
|
| Mon, 26 Jul 2010 17:26:02 +0200 |
blanchet |
simplify code
|
changeset |
files
|
| Mon, 26 Jul 2010 17:22:39 +0200 |
blanchet |
remove more Skolemization-aware code
|
changeset |
files
|
| Mon, 26 Jul 2010 17:17:59 +0200 |
blanchet |
kill Skolem handling in Sledgehammer
|
changeset |
files
|
| Mon, 26 Jul 2010 17:09:10 +0200 |
blanchet |
simplify "conjecture_shape" business, as a result of using FOF instead of CNF
|
changeset |
files
|
| Mon, 26 Jul 2010 17:03:21 +0200 |
blanchet |
generate full first-order formulas (FOF) in Sledgehammer
|
changeset |
files
|
| Mon, 26 Jul 2010 14:14:24 +0200 |
blanchet |
make TPTP generator accept full first-order formulas
|
changeset |
files
|
| Mon, 26 Jul 2010 11:26:47 +0200 |
blanchet |
generate close formulas for SPASS, but not for the others (to avoid clutter)
|
changeset |
files
|
| Mon, 26 Jul 2010 11:21:25 +0200 |
blanchet |
renamed internal function
|
changeset |
files
|
| Mon, 26 Jul 2010 11:21:11 +0200 |
blanchet |
proof reconstruction for full FOF terms
|
changeset |
files
|
| Mon, 26 Jul 2010 11:19:57 +0200 |
blanchet |
remove confusing line in SPASS output (because the axiom names are off -- bug in SPASS)
|
changeset |
files
|
| Mon, 26 Jul 2010 11:19:21 +0200 |
blanchet |
reorder SPASS conjectures correctly, based on Flotter output
|
changeset |
files
|
| Tue, 27 Jul 2010 12:02:10 +0100 |
paulson |
Deleted an obsolete file
|
changeset |
files
|
| Wed, 28 Jul 2010 00:13:26 +0200 |
wenzelm |
explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;
|
changeset |
files
|
| Wed, 28 Jul 2010 00:03:22 +0200 |
wenzelm |
use file names relative to master directory of theory source -- Proof General can now handle that due to the ThyLoad.add_path deception (cf. 3ceccd415145);
|
changeset |
files
|
| Tue, 27 Jul 2010 23:25:50 +0200 |
wenzelm |
simplified handling of update_time -- do not store within deps;
|
changeset |
files
|
| 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
|
| 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
|
| 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
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
tuned whitespace
|
changeset |
files
|
| Mon, 19 Jul 2010 16:09:43 +0200 |
haftmann |
dropped essentially ineffective tuning
|
changeset |
files
|
| Mon, 19 Jul 2010 16:09:43 +0200 |
haftmann |
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
|
changeset |
files
|
| Mon, 19 Jul 2010 12:17:38 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 19 Jul 2010 12:17:30 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 19 Jul 2010 11:55:44 +0200 |
haftmann |
distinguish different classes of const syntax
|
changeset |
files
|
| Mon, 19 Jul 2010 11:55:43 +0200 |
haftmann |
Scala: subtle difference in printing strings vs. complex mixfix syntax
|
changeset |
files
|
| Mon, 19 Jul 2010 11:55:42 +0200 |
haftmann |
check code generation for Scala
|
changeset |
files
|
| Mon, 19 Jul 2010 11:55:42 +0200 |
haftmann |
dropped superfluous prefixes
|
changeset |
files
|
| Mon, 19 Jul 2010 11:55:42 +0200 |
haftmann |
optional break
|
changeset |
files
|
| Fri, 16 Jul 2010 15:55:32 +0200 |
haftmann |
consolidate const_syntax naming
|
changeset |
files
|
| Wed, 21 Jul 2010 16:49:52 +0200 |
wenzelm |
recovered benchmarks, which are not tested automatically;
|
changeset |
files
|
| Wed, 21 Jul 2010 16:29:20 +0200 |
wenzelm |
reactivate SML/NJ test on macbroy28, while macbroy23 is unavailable;
|
changeset |
files
|