| Sat, 19 Sep 2009 07:38:03 +0200 |
haftmann |
inter and union are mere abbreviations for inf and sup
|
changeset |
files
|
| Thu, 24 Sep 2009 19:14:18 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 24 Sep 2009 18:29:29 +0200 |
haftmann |
lemma relating fold1 and foldl; code_unfold rules for Inf_fin, Sup_fin, Min, Max, Inf, Sup
|
changeset |
files
|
| Thu, 24 Sep 2009 18:29:29 +0200 |
haftmann |
subsumed by more general setup in List.thy
|
changeset |
files
|
| Thu, 24 Sep 2009 18:29:29 +0200 |
haftmann |
idempotency case for fold1
|
changeset |
files
|
| Thu, 24 Sep 2009 18:29:28 +0200 |
haftmann |
added dual for complete lattice
|
changeset |
files
|
| Thu, 24 Sep 2009 17:26:05 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 24 Sep 2009 17:25:42 +0200 |
nipkow |
record how many "proof"s are solved by s/h
|
changeset |
files
|
| Thu, 24 Sep 2009 15:00:17 +0200 |
boehmes |
added quotes for filenames;
|
changeset |
files
|
| Thu, 24 Sep 2009 08:28:27 +0200 |
bulwahn |
merged; adopted to changes from Code_Evaluation in the predicate compiler
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:13 +0200 |
bulwahn |
replaced sorry by oops; removed old debug functions in predicate compiler
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:13 +0200 |
bulwahn |
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
adapted configuration for DatatypeCase.make_case
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added a new example for the predicate compiler
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added first prototype of the extended predicate compiler
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
moved predicate compiler to Tools
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
removed generation of strange tuple modes in predicate compiler
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
extending predicate compiler and proof procedure to support tuples; testing predicate wirh HOL-MicroJava semantics
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
modified predicate compiler further to support tuples
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
changed preprocessing due to problems with LightweightJava; added transfer of thereoms; changed the type of mode to support tuples in the predicate compiler
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
handling of definitions
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
experimenting to add some useful interface for definitions
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added predicate compile preprocessing structure for definitional thms -- probably is replaced by hooking the theorem command differently
|
changeset |
files
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
modified handling of side conditions in proof procedure of predicate compiler
|
changeset |
files
|
| Wed, 23 Sep 2009 15:25:25 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 23 Sep 2009 14:00:12 +0200 |
haftmann |
Code_Eval(uation)
|
changeset |
files
|
| Wed, 23 Sep 2009 13:48:16 +0200 |
blanchet |
merged
|
changeset |
files
|
| Wed, 23 Sep 2009 13:47:08 +0200 |
blanchet |
Added "nitpick_const_simp" tags to lazy list theories.
|
changeset |
files
|
| Wed, 23 Sep 2009 13:48:35 +0200 |
krauss |
atbroy101 is long dead, use atbroy99; comment out broken SML test invocation
|
changeset |
files
|
| Wed, 23 Sep 2009 13:42:53 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 23 Sep 2009 12:03:47 +0200 |
haftmann |
stripped legacy ML bindings
|
changeset |
files
|
| Wed, 23 Sep 2009 13:31:38 +0200 |
hoelzl |
Undo errornous commit of Statespace change
|
changeset |
files
|
| Wed, 23 Sep 2009 13:17:17 +0200 |
hoelzl |
correct variable order in approximate-method
|
changeset |
files
|
| Wed, 23 Sep 2009 11:06:32 +0100 |
paulson |
merged
|
changeset |
files
|
| Wed, 23 Sep 2009 11:05:28 +0100 |
paulson |
Correct chasing of type variable instantiations during type unification.
|
changeset |
files
|
| Wed, 23 Sep 2009 11:33:52 +0200 |
haftmann |
hide newly introduced constants
|
changeset |
files
|
| Tue, 22 Sep 2009 11:26:46 +0200 |
Philipp Meyer |
used standard fold function and type aliases
|
changeset |
files
|
| Mon, 21 Sep 2009 15:05:26 +0200 |
Philipp Meyer |
sos method generates and uses proof certificates
|
changeset |
files
|
| Tue, 22 Sep 2009 20:25:31 +0200 |
wenzelm |
full reserve of worker threads -- for improved CPU utilization;
|
changeset |
files
|
| Tue, 22 Sep 2009 15:38:12 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 22 Sep 2009 15:36:55 +0200 |
haftmann |
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
|
changeset |
files
|
| Tue, 22 Sep 2009 15:12:45 +0200 |
krauss |
tail -n 20: more helpful output if make fails
|
changeset |
files
|
| Tue, 22 Sep 2009 08:58:08 +0200 |
haftmann |
corrected order of type variables in code equations; more precise certificate for cases
|
changeset |
files
|
| Mon, 21 Sep 2009 16:16:16 +0200 |
Christian Urban |
merged
|
changeset |
files
|
| Mon, 21 Sep 2009 15:02:23 +0200 |
Christian Urban |
tuned some proofs
|
changeset |
files
|
| Mon, 21 Sep 2009 16:11:36 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 21 Sep 2009 16:01:38 +0200 |
haftmann |
added session theory for Bali and Nominal_Examples
|
changeset |
files
|
| Mon, 21 Sep 2009 16:01:30 +0200 |
haftmann |
added session theory for Nominal_Examples
|
changeset |
files
|
| Mon, 21 Sep 2009 16:00:53 +0200 |
haftmann |
added session theory for Bali
|
changeset |
files
|
| Mon, 21 Sep 2009 16:00:34 +0200 |
haftmann |
adjusted to new Number Theory scenario
|
changeset |
files
|
| Mon, 21 Sep 2009 15:33:40 +0200 |
haftmann |
added session entry point theories
|
changeset |
files
|
| Mon, 21 Sep 2009 15:33:40 +0200 |
haftmann |
common base for protocols with symmetric keys
|
changeset |
files
|
| Mon, 21 Sep 2009 15:33:39 +0200 |
haftmann |
tuned header
|
changeset |
files
|
| Mon, 21 Sep 2009 14:22:32 +0200 |
haftmann |
isarified proof
|
changeset |
files
|
| Mon, 21 Sep 2009 16:07:20 +0200 |
wenzelm |
fixed permissions -- this is a script, not an executable;
|
changeset |
files
|
| Mon, 21 Sep 2009 16:06:52 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 21 Sep 2009 13:42:36 +0200 |
boehmes |
deleted unused file
|
changeset |
files
|
| Mon, 21 Sep 2009 12:23:05 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 21 Sep 2009 12:22:53 +0200 |
haftmann |
entry point theory for examples; reactivated half-dead example
|
changeset |
files
|
| Mon, 21 Sep 2009 11:15:55 +0200 |
boehmes |
merged
|
changeset |
files
|
| Mon, 21 Sep 2009 11:15:21 +0200 |
boehmes |
corrected remote SMT solver invocation
|
changeset |
files
|
| Mon, 21 Sep 2009 10:58:25 +0200 |
haftmann |
theory entry point for session Hoare_Parallel (now also with proper underscore)
|
changeset |
files
|
| Mon, 21 Sep 2009 08:45:31 +0200 |
boehmes |
merged
|
changeset |
files
|
| Mon, 21 Sep 2009 08:34:56 +0200 |
boehmes |
tuned author
|
changeset |
files
|
| Fri, 18 Sep 2009 18:13:19 +0200 |
boehmes |
added new method "smt": an oracle-based connection to external SMT solvers
|
changeset |
files
|
| Sun, 20 Sep 2009 19:17:33 +0200 |
wenzelm |
tuned tracing;
|
changeset |
files
|
| Sun, 20 Sep 2009 18:37:55 +0200 |
wenzelm |
scheduler backdoor: 9999 means 1 worker;
|
changeset |
files
|
| Sun, 20 Sep 2009 18:15:07 +0200 |
wenzelm |
Hilbert_Classical: more precise control of parallel_proofs;
|
changeset |
files
|
| Sun, 20 Sep 2009 17:23:23 +0200 |
wenzelm |
actually observe Multithreading.enabled (cf. d302f1c9e356);
|
changeset |
files
|
| Sat, 19 Sep 2009 10:19:34 +0200 |
nipkow |
merged
|
changeset |
files
|
| Sat, 19 Sep 2009 10:19:12 +0200 |
nipkow |
restructured code
|
changeset |
files
|
| Sat, 19 Sep 2009 07:35:27 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 18 Sep 2009 16:00:56 +0200 |
haftmann |
rewrite premises in tactical proof also with inf_fun_eq and inf_bool_eq: attempt to allow user to use inf [=>] and inf [bool] in his specs
|
changeset |
files
|
| Fri, 18 Sep 2009 23:08:53 +0200 |
nipkow |
modified minimization log
|
changeset |
files
|
| Fri, 18 Sep 2009 14:40:24 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 18 Sep 2009 14:40:06 +0200 |
nipkow |
skip &&& goals
|
changeset |
files
|
| Fri, 18 Sep 2009 14:09:38 +0200 |
haftmann |
INTER and UNION are mere abbreviations for INFI and SUPR
|
changeset |
files
|
| Fri, 18 Sep 2009 09:35:23 +0200 |
haftmann |
simplified proof
|
changeset |
files
|
| Fri, 18 Sep 2009 09:07:51 +0200 |
haftmann |
partially isarified proof
|
changeset |
files
|
| Fri, 18 Sep 2009 09:07:50 +0200 |
haftmann |
tuned const_name antiquotations
|
changeset |
files
|
| Fri, 18 Sep 2009 09:07:49 +0200 |
haftmann |
more antiquotations
|
changeset |
files
|
| Fri, 18 Sep 2009 09:07:48 +0200 |
haftmann |
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
|
changeset |
files
|
| Fri, 18 Sep 2009 07:54:26 +0200 |
haftmann |
tuned NEWS, added CONTRIBUTORS
|
changeset |
files
|
| Thu, 17 Sep 2009 19:13:22 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 17 Sep 2009 19:13:07 +0200 |
nipkow |
removed misleading log line
|
changeset |
files
|
| Thu, 17 Sep 2009 15:04:46 +0100 |
paulson |
NEWS: New method metisFT
|
changeset |
files
|
| Thu, 17 Sep 2009 14:59:58 +0100 |
paulson |
New theorems for proving equalities and inclusions involving unions
|
changeset |
files
|
| Thu, 17 Sep 2009 14:07:44 +0200 |
boehmes |
added time limit for extraction phase (not supported on Cygwin)
|
changeset |
files
|
| Thu, 17 Sep 2009 11:58:21 +0200 |
boehmes |
merged
|
changeset |
files
|
| Thu, 17 Sep 2009 11:57:36 +0200 |
boehmes |
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
|
changeset |
files
|
| Wed, 16 Sep 2009 22:46:10 +0200 |
wenzelm |
Synchronized.value does not require locking, since assigments are atomic;
|
changeset |
files
|
| Wed, 16 Sep 2009 21:31:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 16 Sep 2009 21:14:08 +0200 |
wenzelm |
replaced opaque signature matching by plain old abstype (again, cf. ac4498f95d1c) -- this recovers pretty printing in SML/NJ and Poly/ML 5.3;
|
changeset |
files
|
| Wed, 16 Sep 2009 13:43:15 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 16 Sep 2009 13:43:07 +0200 |
haftmann |
Inter and Union are mere abbreviations for Inf and Sup; tuned
|
changeset |
files
|
| Wed, 16 Sep 2009 13:43:05 +0200 |
haftmann |
Inter and Union are mere abbreviations for Inf and Sup
|
changeset |
files
|
| Wed, 16 Sep 2009 13:03:03 +0200 |
nipkow |
merged
|
changeset |
files
|
| Wed, 16 Sep 2009 12:47:14 +0200 |
nipkow |
revised lemma counting
|
changeset |
files
|
| Wed, 16 Sep 2009 09:04:41 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 15 Sep 2009 19:16:47 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 15 Sep 2009 19:16:35 +0200 |
haftmann |
hide new constants
|
changeset |
files
|
| Tue, 15 Sep 2009 15:41:30 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 15 Sep 2009 15:41:23 +0200 |
haftmann |
restored code generation for OCaml
|
changeset |
files
|
| Tue, 15 Sep 2009 15:22:15 +0200 |
haftmann |
added singleton example
|
changeset |
files
|
| Tue, 15 Sep 2009 12:11:10 +0200 |
haftmann |
added emptiness check predicate and singleton projection
|
changeset |
files
|
| Wed, 16 Sep 2009 00:12:52 +0200 |
wenzelm |
added append_after (tuned version of former insert_after of Seq);
|
changeset |
files
|
| Tue, 15 Sep 2009 23:57:07 +0200 |
wenzelm |
double linking for improved performance of "prev";
|
changeset |
files
|
| Tue, 15 Sep 2009 15:44:57 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 15 Sep 2009 15:29:11 +0200 |
boehmes |
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
|
changeset |
files
|
| Tue, 15 Sep 2009 15:17:53 +0200 |
wenzelm |
Isar.define_command: identify transaction;
|
changeset |
files
|
| Tue, 15 Sep 2009 13:09:13 +0200 |
wenzelm |
updated bib;
|
changeset |
files
|
| Mon, 14 Sep 2009 19:30:48 +0200 |
nipkow |
count number of iterations required for minimization (and fixed bug: minimization was always called)
|
changeset |
files
|
| Mon, 14 Sep 2009 12:25:02 +0200 |
haftmann |
merged
|
changeset |
files
|
| Mon, 14 Sep 2009 08:36:58 +0200 |
haftmann |
more antiquotations
|
changeset |
files
|
| Mon, 14 Sep 2009 08:36:57 +0200 |
haftmann |
some lemmas about strict order in lattices
|
changeset |
files
|
| Sun, 13 Sep 2009 02:10:41 +0200 |
wenzelm |
explicitly export type abbreviations (as usual in SML97);
|
changeset |
files
|
| Sun, 13 Sep 2009 02:07:52 +0200 |
wenzelm |
wrapper for Real.fmt -- via StringCvt.realfmt;
|
changeset |
files
|
| Sun, 13 Sep 2009 02:07:06 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Sat, 12 Sep 2009 16:30:48 +0200 |
wenzelm |
standard headers and text sections;
|
changeset |
files
|
| Fri, 11 Sep 2009 09:53:02 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 11 Sep 2009 09:52:40 +0200 |
nipkow |
Made record parameter flexible to allow for extensions
|
changeset |
files
|
| Fri, 11 Sep 2009 09:05:26 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 11 Sep 2009 09:04:51 +0200 |
haftmann |
corrected upper/lowercase
|
changeset |
files
|
| Thu, 10 Sep 2009 17:14:05 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 10 Sep 2009 15:26:51 +0200 |
haftmann |
obey underscore naming convention
|
changeset |
files
|
| Thu, 10 Sep 2009 15:23:09 +0200 |
haftmann |
plain structure name; signature constraint; shorter lines
|
changeset |
files
|
| Thu, 10 Sep 2009 15:23:08 +0200 |
haftmann |
split of test examples from NatTransfer
|
changeset |
files
|
| Thu, 10 Sep 2009 15:23:08 +0200 |
haftmann |
generic transfer procedure
|
changeset |
files
|
| Thu, 10 Sep 2009 15:23:07 +0200 |
haftmann |
early bootstrap of generic transfer procedure
|
changeset |
files
|
| Thu, 10 Sep 2009 14:07:58 +0200 |
haftmann |
cleanedup theorems all_nat ex_nat
|
changeset |
files
|
| Thu, 10 Sep 2009 16:16:18 +0200 |
Philipp Meyer |
atp_minimize is now not using whitelist
|
changeset |
files
|
| Thu, 10 Sep 2009 15:57:55 +0200 |
nipkow |
position information is now passed to all actions;
|
changeset |
files
|
| Thu, 10 Sep 2009 12:53:49 +0200 |
nipkow |
logging number of metis lemmas
|
changeset |
files
|
| Wed, 09 Sep 2009 23:26:34 +0200 |
nipkow |
minimization: comparing w/ and w/o.
|
changeset |
files
|
| Wed, 09 Sep 2009 12:29:06 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 09 Sep 2009 12:24:22 +0200 |
haftmann |
dropped accidental code additions
|
changeset |
files
|
| Wed, 09 Sep 2009 12:27:41 +0200 |
haftmann |
merged
|
changeset |
files
|
| Wed, 09 Sep 2009 12:27:12 +0200 |
haftmann |
explicit transfer avoids spurious merge problems
|
changeset |
files
|
| Wed, 09 Sep 2009 11:31:20 +0200 |
haftmann |
moved eq handling in nbe into separate oracle
|
changeset |
files
|
| Tue, 08 Sep 2009 18:31:26 +0200 |
wenzelm |
tuned document -- proper text instead of source comments, reduced line length;
|
changeset |
files
|
| Tue, 01 Sep 2009 11:19:49 +0200 |
Philipp Meyer |
fixed cleanup routine in neos csdp script
|
changeset |
files
|
| Tue, 08 Sep 2009 09:57:33 +0200 |
boehmes |
timeout option for ATPs
|
changeset |
files
|
| Mon, 07 Sep 2009 22:13:32 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 07 Sep 2009 22:12:16 +0200 |
wenzelm |
modernized Event_Bus -- based on actors;
|
changeset |
files
|
| Mon, 07 Sep 2009 22:08:05 +0200 |
nipkow |
Fixed "minimal" to cover the case that "p []" holds (excluded in the article by Bradley & Manna)
|
changeset |
files
|
| Mon, 07 Sep 2009 19:41:30 +0200 |
nipkow |
merged
|
changeset |
files
|
| Mon, 07 Sep 2009 19:41:07 +0200 |
nipkow |
tuned stats
|
changeset |
files
|
| Mon, 07 Sep 2009 17:02:15 +0100 |
paulson |
Fixed a few problems with the method metisFT
|
changeset |
files
|
| Mon, 07 Sep 2009 16:25:12 +0200 |
nipkow |
merged
|
changeset |
files
|
| Mon, 07 Sep 2009 16:24:32 +0200 |
nipkow |
tuned stats
|
changeset |
files
|
| Mon, 07 Sep 2009 13:19:09 +0100 |
paulson |
My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
|
changeset |
files
|
| Mon, 07 Sep 2009 11:44:12 +0100 |
paulson |
merged
|
changeset |
files
|
| Mon, 07 Sep 2009 10:04:17 +0100 |
paulson |
conflict resolution possibly
|
changeset |
files
|
| Fri, 04 Sep 2009 11:37:24 +0100 |
paulson |
New method, metisFT: a fully-typed proof search that should eliminate type errors during reconstruction
|
changeset |
files
|
| Fri, 28 Aug 2009 13:32:20 +0100 |
paulson |
merged
|
changeset |
files
|
| Thu, 27 Aug 2009 15:49:45 +0100 |
paulson |
More streamlining using metis.
|
changeset |
files
|
| Mon, 07 Sep 2009 08:32:22 +0200 |
nipkow |
enabled metis permanently, tuned stats
|
changeset |
files
|
| Sat, 05 Sep 2009 22:01:31 +0200 |
boehmes |
added signature ATP_MINIMAL,
|
changeset |
files
|
| Sat, 05 Sep 2009 17:35:05 +0200 |
boehmes |
merged
|
changeset |
files
|
| Sat, 05 Sep 2009 17:34:30 +0200 |
boehmes |
separate output of ATP user time and sledgehammer (ML code) user time
|
changeset |
files
|
| Sat, 05 Sep 2009 15:46:52 +0200 |
boehmes |
Mirabelle: command-line action options may either be key=value or just key
|
changeset |
files
|
| Sat, 05 Sep 2009 11:45:57 +0200 |
boehmes |
added initialization and cleanup of actions,
|
changeset |
files
|
| Fri, 04 Sep 2009 15:19:51 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 04 Sep 2009 15:18:35 +0200 |
haftmann |
tuned metis proofs
|
changeset |
files
|
| Fri, 04 Sep 2009 13:57:56 +0200 |
boehmes |
tuned
|
changeset |
files
|
| Fri, 04 Sep 2009 10:58:50 +0200 |
nipkow |
tuned output
|
changeset |
files
|
| Thu, 03 Sep 2009 22:48:18 +0200 |
boehmes |
merged
|
changeset |
files
|
| Thu, 03 Sep 2009 22:47:31 +0200 |
boehmes |
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
|
changeset |
files
|
| Thu, 03 Sep 2009 20:26:07 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 03 Sep 2009 17:26:10 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 03 Sep 2009 15:39:02 +0200 |
haftmann |
proper class syntax for sublocale class < expr
|
changeset |
files
|
| Thu, 03 Sep 2009 18:41:58 +0200 |
boehmes |
added option full_typed for sledgehammer action
|
changeset |
files
|
| Thu, 03 Sep 2009 17:55:31 +0200 |
boehmes |
added runtime information to sledgehammer
|
changeset |
files
|
| Thu, 03 Sep 2009 15:47:39 +0200 |
boehmes |
tuned
|
changeset |
files
|
| Thu, 03 Sep 2009 15:30:05 +0200 |
nipkow |
scaled avg_time
|
changeset |
files
|
| Thu, 03 Sep 2009 14:50:02 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 03 Sep 2009 14:49:34 +0200 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 03 Sep 2009 14:40:52 +0200 |
krauss |
isatest: collect test results and logs in testdata repository
|
changeset |
files
|
| Thu, 03 Sep 2009 14:31:04 +0200 |
boehmes |
replaced backlist by whitelist
|
changeset |
files
|
| Thu, 03 Sep 2009 14:05:13 +0200 |
boehmes |
Mirabelle: logging of exceptions (works only for PolyML)
|
changeset |
files
|
| Wed, 02 Sep 2009 22:12:40 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 02 Sep 2009 22:12:20 +0200 |
wenzelm |
refined delay into delay_first/delay_last;
|
changeset |
files
|
| Wed, 02 Sep 2009 21:34:13 +0200 |
boehmes |
merged
|
changeset |
files
|
| Wed, 02 Sep 2009 21:33:16 +0200 |
boehmes |
add report script for Mirabelle
|
changeset |
files
|
| Wed, 02 Sep 2009 21:31:58 +0200 |
boehmes |
Mirabelle: actions are responsible for handling exceptions,
|
changeset |
files
|
| Wed, 02 Sep 2009 16:29:50 +0200 |
boehmes |
removed errors overseen in previous changes
|
changeset |
files
|
| Wed, 02 Sep 2009 16:23:53 +0200 |
boehmes |
moved Mirabelle from HOL/Tools to HOL,
|
changeset |
files
|
| Wed, 02 Sep 2009 16:02:37 +0200 |
boehmes |
removed unused signature
|
changeset |
files
|
| Wed, 02 Sep 2009 20:49:04 +0200 |
wenzelm |
explicit checks;
|
changeset |
files
|
| Wed, 02 Sep 2009 17:33:25 +0200 |
wenzelm |
updated Poly/ML SVN version;
|
changeset |
files
|
| Wed, 02 Sep 2009 16:51:19 +0200 |
wenzelm |
eval/location_props: always produce YXML markup, independent of print_mode;
|
changeset |
files
|
| Wed, 02 Sep 2009 16:25:44 +0200 |
wenzelm |
reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
|
changeset |
files
|
| Wed, 02 Sep 2009 14:11:45 +0200 |
wenzelm |
tuned ML message;
|
changeset |
files
|
| Wed, 02 Sep 2009 12:20:17 +0200 |
nipkow |
added "using" to blacklist
|
changeset |
files
|
| Wed, 02 Sep 2009 10:54:52 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 02 Sep 2009 10:35:47 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 01 Sep 2009 21:40:10 +0200 |
wenzelm |
removed old Isar document model;
|
changeset |
files
|
| Tue, 01 Sep 2009 21:46:38 +0200 |
haftmann |
corrected spelling
|
changeset |
files
|
| Tue, 01 Sep 2009 21:44:19 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 01 Sep 2009 17:02:09 +0200 |
haftmann |
added -q switch for run in qnd mode
|
changeset |
files
|
| Tue, 01 Sep 2009 16:39:05 +0200 |
haftmann |
code generator is now a separate component
|
changeset |
files
|
| Tue, 01 Sep 2009 16:00:59 +0200 |
haftmann |
tuned document
|
changeset |
files
|
| Tue, 01 Sep 2009 16:00:57 +0200 |
haftmann |
some reorganization of number theory
|
changeset |
files
|
| Tue, 01 Sep 2009 15:39:33 +0200 |
haftmann |
some reorganization of number theory
|
changeset |
files
|
| Tue, 01 Sep 2009 14:13:34 +0200 |
haftmann |
merged
|
changeset |
files
|
| Tue, 01 Sep 2009 14:12:18 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Mon, 24 Aug 2009 08:31:41 +0200 |
haftmann |
avoid long line
|
changeset |
files
|
| Tue, 01 Sep 2009 19:48:11 +0200 |
nipkow |
added txt to blacklist
|
changeset |
files
|
| Tue, 01 Sep 2009 21:03:04 +0200 |
wenzelm |
Isabelle_Process: receiver as Actor, not EventBus;
|
changeset |
files
|
| Tue, 01 Sep 2009 15:21:22 +0200 |
boehmes |
merged
|
changeset |
files
|
| Tue, 01 Sep 2009 15:20:21 +0200 |
boehmes |
Mirabelle: actions are responsible for their log messages, output is better readable
|
changeset |
files
|
| Tue, 01 Sep 2009 14:57:03 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 01 Sep 2009 14:10:38 +0200 |
boehmes |
merged
|
changeset |
files
|
| Tue, 01 Sep 2009 14:09:59 +0200 |
boehmes |
Mirabelle: added preliminary documentation,
|
changeset |
files
|
| Mon, 31 Aug 2009 19:28:37 +0200 |
boehmes |
Mirabelle: explicit command blacklist, preliminary documentation
|
changeset |
files
|
| Tue, 01 Sep 2009 14:51:40 +0200 |
wenzelm |
modernized Isar_Document;
|
changeset |
files
|
| Tue, 01 Sep 2009 14:45:06 +0200 |
wenzelm |
modernized Thy_Header;
|
changeset |
files
|
| Tue, 01 Sep 2009 13:31:22 +0200 |
wenzelm |
misc cleanup and internal reorganization;
|
changeset |
files
|
| Tue, 01 Sep 2009 11:52:19 +0200 |
wenzelm |
added linear_set.scala from http://isabelle.in.tum.de/repos/isabelle-jedit/rev/d567692f9717
|
changeset |
files
|
| Mon, 31 Aug 2009 20:34:48 +0200 |
krauss |
moved lemma Wellfounded.in_inv_image to Relation.thy
|
changeset |
files
|
| Mon, 31 Aug 2009 20:34:44 +0200 |
krauss |
moved wfrec to Recdef.thy
|
changeset |
files
|
| Mon, 31 Aug 2009 20:32:00 +0200 |
krauss |
no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
|
changeset |
files
|
| Mon, 31 Aug 2009 17:32:29 +0200 |
boehmes |
Mirabelle: handle possible parser exceptions, emit suitable log message
|
changeset |
files
|
| Mon, 31 Aug 2009 15:30:11 +0200 |
boehmes |
merged
|
changeset |
files
|
| Mon, 31 Aug 2009 15:29:26 +0200 |
boehmes |
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
|
changeset |
files
|
| Mon, 31 Aug 2009 14:10:11 +0200 |
nipkow |
merged
|
changeset |
files
|
| Mon, 31 Aug 2009 14:09:42 +0200 |
nipkow |
tuned the simp rules for Int involving insert and intervals.
|
changeset |
files
|
| Mon, 31 Aug 2009 12:22:15 +0200 |
boehmes |
Mirabelle sledgehammer: added option to keep problem files, enabled "metis" switch again (was accidentally removed)
|
changeset |
files
|
| Mon, 31 Aug 2009 09:28:50 +0200 |
boehmes |
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
|
changeset |
files
|
| Sat, 29 Aug 2009 22:01:55 +0200 |
boehmes |
merged
|
changeset |
files
|
| Sat, 29 Aug 2009 21:58:33 +0200 |
boehmes |
apply metis with found theorems in case sledgehammer was successful
|
changeset |
files
|
| Sat, 29 Aug 2009 21:57:06 +0200 |
boehmes |
propagate theorem names, in addition to generated return message
|
changeset |
files
|
| Sat, 29 Aug 2009 14:31:39 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Sat, 29 Aug 2009 12:01:25 +0200 |
wenzelm |
eliminated hard tabs;
|
changeset |
files
|
| Sat, 29 Aug 2009 10:50:04 +0200 |
wenzelm |
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
|
changeset |
files
|
| Fri, 28 Aug 2009 21:44:48 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 28 Aug 2009 20:49:53 +0200 |
krauss |
fixed HOLogic.stringT
|
changeset |
files
|
| Fri, 28 Aug 2009 20:22:12 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 28 Aug 2009 20:21:50 +0200 |
nipkow |
tuned proofs
|
changeset |
files
|