wenzelm [Tue, 14 Feb 2012 17:49:47 +0100] rev 46461
eliminated unused subgoals_tac;
wenzelm [Tue, 14 Feb 2012 17:26:35 +0100] rev 46460
eliminated obsolete aliases;
wenzelm [Tue, 14 Feb 2012 17:11:33 +0100] rev 46459
eliminated obsolete aliases;
wenzelm [Tue, 14 Feb 2012 16:59:12 +0100] rev 46458
tuned;
wenzelm [Tue, 14 Feb 2012 12:40:55 +0100] rev 46457
merged, resolving trivial conflicts;
wenzelm [Tue, 14 Feb 2012 11:16:07 +0100] rev 46456
merged;
blanchet [Sat, 11 Feb 2012 13:41:36 +0100] rev 46455
new SPASS options
bulwahn [Sat, 11 Feb 2012 12:13:08 +0100] rev 46454
making num_mutations a configuration that can be changed with the mutabelle bash command
bulwahn [Sat, 11 Feb 2012 11:36:23 +0100] rev 46453
making max_mutants an option that can be changed in the Mutabelle-script
bulwahn [Sat, 11 Feb 2012 11:36:21 +0100] rev 46452
increase timeout to 30 seconds; changing mutabelle script
blanchet [Fri, 10 Feb 2012 17:10:49 +0100] rev 46451
parse clauses generated from several formulas
blanchet [Fri, 10 Feb 2012 17:10:47 +0100] rev 46450
be more gentle when generating KBO weights
blanchet [Fri, 10 Feb 2012 16:33:58 +0100] rev 46449
update SPASS slices
Cezary Kaliszyk <cezarykaliszyk@gmail.com> [Fri, 10 Feb 2012 09:47:59 +0100] rev 46448
more specification of the quotient package in IsarRef
Cezary Kaliszyk <cezarykaliszyk@gmail.com> [Fri, 10 Feb 2012 09:02:51 +0100] rev 46447
specification of the quotient package
blanchet [Thu, 09 Feb 2012 16:00:04 +0100] rev 46446
tune KBO weight code
blanchet [Thu, 09 Feb 2012 14:42:18 +0100] rev 46445
minor DFG fix
blanchet [Thu, 09 Feb 2012 14:35:27 +0100] rev 46444
new SPASS slices
blanchet [Thu, 09 Feb 2012 14:04:17 +0100] rev 46443
improved KBO weights -- beware of explicit applications
blanchet [Thu, 09 Feb 2012 12:57:59 +0100] rev 46442
added possibility of generating KBO weights to DFG problems
Cezary Kaliszyk <cezarykaliszyk@gmail.com> [Thu, 09 Feb 2012 09:36:30 +0100] rev 46441
Generalize the compositional preservation theorems
blanchet [Wed, 08 Feb 2012 01:49:33 +0100] rev 46440
use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
blanchet [Wed, 08 Feb 2012 00:55:06 +0100] rev 46439
removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly
blanchet [Wed, 08 Feb 2012 00:05:22 +0100] rev 46438
beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms
blanchet [Mon, 06 Feb 2012 23:01:02 +0100] rev 46437
fixed arity error
blanchet [Mon, 06 Feb 2012 23:01:02 +0100] rev 46436
tuning
blanchet [Mon, 06 Feb 2012 23:01:01 +0100] rev 46435
renamed type encoding
bulwahn [Sun, 05 Feb 2012 17:43:15 +0100] rev 46434
adding some forbidden constant names for mutabelle
bulwahn [Sun, 05 Feb 2012 17:43:14 +0100] rev 46433
mutabelle ignores theorems with internal constants
nipkow [Sun, 05 Feb 2012 17:09:21 +0100] rev 46432
tuned
nipkow [Sun, 05 Feb 2012 16:53:20 +0100] rev 46431
merged
nipkow [Sun, 05 Feb 2012 16:53:11 +0100] rev 46430
simplified code generation
blanchet [Sun, 05 Feb 2012 13:28:51 +0100] rev 46429
remove option that's on by default
blanchet [Sun, 05 Feb 2012 12:27:10 +0100] rev 46428
no need for a script/mega-hack with the new SPASS
blanchet [Sun, 05 Feb 2012 12:27:10 +0100] rev 46427
cleaned up new SPASS parsing
blanchet [Sun, 05 Feb 2012 12:27:10 +0100] rev 46426
tuning
bulwahn [Sun, 05 Feb 2012 11:14:25 +0100] rev 46425
merged
bulwahn [Sun, 05 Feb 2012 10:43:52 +0100] rev 46424
adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists
bulwahn [Sun, 05 Feb 2012 10:42:57 +0100] rev 46423
tuning to remove ML warnings
blanchet [Sun, 05 Feb 2012 10:50:34 +0100] rev 46422
removed double filtering of type args
bulwahn [Sun, 05 Feb 2012 08:57:03 +0100] rev 46421
adding a quickcheck example about functions and sets
bulwahn [Sun, 05 Feb 2012 08:47:13 +0100] rev 46420
removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)
bulwahn [Sun, 05 Feb 2012 08:36:41 +0100] rev 46419
adding a remark about lemma which is too special and should be removed
bulwahn [Sun, 05 Feb 2012 08:24:39 +0100] rev 46418
another try to improve code generation of set equality (cf. da32cf32c0c7)
bulwahn [Sun, 05 Feb 2012 08:24:38 +0100] rev 46417
beautifying definitions of check_all and adding instance for finite_4
Cezary Kaliszyk <cezarykaliszyk@gmail.com> [Sun, 05 Feb 2012 07:05:34 +0100] rev 46416
Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
blanchet [Sat, 04 Feb 2012 17:01:25 +0100] rev 46415
added option to Mirabelle/Sledgehammer
blanchet [Sat, 04 Feb 2012 12:08:18 +0100] rev 46414
improved hashing w.r.t. Mirabelle, to help debugging
blanchet [Sat, 04 Feb 2012 12:08:18 +0100] rev 46413
tuned SPASS DFG output
blanchet [Sat, 04 Feb 2012 12:08:18 +0100] rev 46412
the new SPASS gives accurate fact information, so no need for old hack anymore
blanchet [Sat, 04 Feb 2012 12:08:18 +0100] rev 46411
fixed docs
blanchet [Sat, 04 Feb 2012 12:08:18 +0100] rev 46410
made sure to filter type args also for "uncurried alias" equations
blanchet [Sat, 04 Feb 2012 12:08:18 +0100] rev 46409
made option available to users (mostly for experiments)
bulwahn [Sat, 04 Feb 2012 07:40:02 +0100] rev 46408
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a)
blanchet [Fri, 03 Feb 2012 18:00:55 +0100] rev 46407
optimization: slice caching in case two consecutive slices are nearly identical
blanchet [Fri, 03 Feb 2012 18:00:55 +0100] rev 46406
extended SPASS/DFG output with ranks
blanchet [Fri, 03 Feb 2012 18:00:55 +0100] rev 46405
try to pass fewer options to Metis
Cezary Kaliszyk <cezarykaliszyk@gmail.com> [Fri, 03 Feb 2012 15:51:10 +0100] rev 46404
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
blanchet [Thu, 02 Feb 2012 19:41:58 +0100] rev 46403
improve SPASS scripts
blanchet [Thu, 02 Feb 2012 15:14:18 +0100] rev 46402
change 9ce354a77908 wasn't quite right -- here's an improvement
blanchet [Thu, 02 Feb 2012 12:51:03 +0100] rev 46401
better SPASS setup
blanchet [Thu, 02 Feb 2012 12:42:05 +0100] rev 46400
don't introduce new symbols in helpers -- makes problems unprovable
blanchet [Thu, 02 Feb 2012 12:42:05 +0100] rev 46399
only constants can be aliased
blanchet [Thu, 02 Feb 2012 12:42:05 +0100] rev 46398
include new SPASS by default if available
bulwahn [Thu, 02 Feb 2012 10:16:10 +0100] rev 46397
adding an example for finite and cofinite sets
bulwahn [Thu, 02 Feb 2012 10:12:30 +0100] rev 46396
adding a minimally refined equality on sets for code generation
bulwahn [Thu, 02 Feb 2012 10:12:11 +0100] rev 46395
adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn [Wed, 01 Feb 2012 15:28:02 +0100] rev 46394
improving code equations for multisets that violated the distinct AList abstraction
blanchet [Thu, 02 Feb 2012 01:55:17 +0100] rev 46393
tuning
blanchet [Thu, 02 Feb 2012 01:20:28 +0100] rev 46392
implemented partial application aliases (for SPASS mainly)
blanchet [Wed, 01 Feb 2012 17:16:55 +0100] rev 46391
really fixed syntax bug in DFG output (cf. ef62c2fafa9e)
blanchet [Wed, 01 Feb 2012 17:15:06 +0100] rev 46390
don't stumble on SPASS debug output
blanchet [Wed, 01 Feb 2012 14:53:46 +0100] rev 46389
tuning
blanchet [Wed, 01 Feb 2012 12:47:43 +0100] rev 46388
proper statuses for "fact_from_ref"
nipkow [Tue, 31 Jan 2012 19:38:36 +0100] rev 46387
tuned
blanchet [Tue, 31 Jan 2012 18:46:31 +0100] rev 46386
renamed Sledgehammer option
blanchet [Tue, 31 Jan 2012 17:09:08 +0100] rev 46385
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
blanchet [Tue, 31 Jan 2012 16:11:15 +0100] rev 46384
improve SPASS setup
bulwahn [Tue, 31 Jan 2012 15:39:45 +0100] rev 46383
adding code equation for setsum
blanchet [Tue, 31 Jan 2012 15:13:18 +0100] rev 46382
avoid name clash, really
blanchet [Tue, 31 Jan 2012 15:10:03 +0100] rev 46381
fixed syntax bug in DFG output
blanchet [Tue, 31 Jan 2012 14:39:21 +0100] rev 46380
new SPASS setup
blanchet [Tue, 31 Jan 2012 12:43:48 +0100] rev 46379
distinguish between ":lr" and ":lt" (terminating) in DFG format
blanchet [Tue, 31 Jan 2012 10:29:05 +0100] rev 46378
nicer keyword class avoidance scheme
blanchet [Tue, 31 Jan 2012 10:29:04 +0100] rev 46377
new try at lambda-lifting that works correctly for both Metis and Sledgehammer (cf. d724066ff3d0)
bulwahn [Tue, 31 Jan 2012 09:06:27 +0100] rev 46376
mutabelle must handle the case where quickcheck returns multiple results
blanchet [Tue, 31 Jan 2012 08:52:47 +0100] rev 46375
reverted e2b1a86d59fc -- broke Metis's lambda-lifting
nipkow [Tue, 31 Jan 2012 07:11:20 +0100] rev 46374
merged
nipkow [Tue, 31 Jan 2012 07:11:04 +0100] rev 46373
NEWS
nipkow [Mon, 30 Jan 2012 21:49:41 +0100] rev 46372
added "'a rel"
blanchet [Mon, 30 Jan 2012 22:56:09 +0100] rev 46371
fix debilitating bug with lambda lifting in conjectures with outer existential quantifiers
blanchet [Mon, 30 Jan 2012 17:18:58 +0100] rev 46370
new SPASS setup
blanchet [Mon, 30 Jan 2012 17:15:59 +0100] rev 46369
example tuning
blanchet [Mon, 30 Jan 2012 17:15:59 +0100] rev 46368
implemented new lambda translations scheme
blanchet [Mon, 30 Jan 2012 17:15:59 +0100] rev 46367
avoid unsupported case in Metis
blanchet [Mon, 30 Jan 2012 17:15:59 +0100] rev 46366
docs and news
blanchet [Mon, 30 Jan 2012 17:15:59 +0100] rev 46365
rename lambda translation schemes
blanchet [Mon, 30 Jan 2012 17:15:59 +0100] rev 46364
example tuning
bulwahn [Mon, 30 Jan 2012 13:55:28 +0100] rev 46363
NEWS
bulwahn [Mon, 30 Jan 2012 13:55:26 +0100] rev 46362
renaming all lemmas with name rel_pow to relpow
bulwahn [Mon, 30 Jan 2012 13:55:24 +0100] rev 46361
adding code equations for max_extp and mlex
bulwahn [Mon, 30 Jan 2012 13:55:23 +0100] rev 46360
adding code generation for relpow by copying the ideas for code generation of funpow
bulwahn [Mon, 30 Jan 2012 13:55:22 +0100] rev 46359
adding code equation for rtranclp in Enum
bulwahn [Mon, 30 Jan 2012 13:55:21 +0100] rev 46358
adding code equation for max_ext
bulwahn [Mon, 30 Jan 2012 13:55:20 +0100] rev 46357
adding code equation for tranclp
bulwahn [Mon, 30 Jan 2012 13:55:19 +0100] rev 46356
adding code_unfold to make measure executable
nipkow [Sun, 29 Jan 2012 15:16:27 +0100] rev 46355
removed accidental dependance of abstract interpreter on gamma
nipkow [Sun, 29 Jan 2012 10:34:02 +0100] rev 46354
merged
nipkow [Sun, 29 Jan 2012 10:33:54 +0100] rev 46353
tuned
bulwahn [Sat, 28 Jan 2012 12:05:26 +0100] rev 46352
an executable version of accessible part (only for finite types yet)
bulwahn [Sat, 28 Jan 2012 10:35:52 +0100] rev 46351
adding yet another induction rule on natural numbers
bulwahn [Sat, 28 Jan 2012 10:22:46 +0100] rev 46350
moving declarations back to the section they seem to belong to (cf. afffe1f72143)
bulwahn [Sat, 28 Jan 2012 06:13:03 +0100] rev 46349
reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code
bulwahn [Fri, 27 Jan 2012 19:08:48 +0100] rev 46348
adding some more examples for quickcheck; replaced FIXME comments
bulwahn [Fri, 27 Jan 2012 17:22:05 +0100] rev 46347
new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well
nipkow [Fri, 27 Jan 2012 17:02:08 +0100] rev 46346
removed duplicate definitions that made locale inconsistent
nipkow [Fri, 27 Jan 2012 14:30:44 +0100] rev 46345
added parity analysis
bulwahn [Fri, 27 Jan 2012 10:31:31 +0100] rev 46344
corrected expectation; added an example for quickcheck
bulwahn [Fri, 27 Jan 2012 10:31:30 +0100] rev 46343
adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck
blanchet [Fri, 27 Jan 2012 10:19:55 +0100] rev 46342
made SML/NJ happy
blanchet [Thu, 26 Jan 2012 20:49:54 +0100] rev 46341
even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant
blanchet [Thu, 26 Jan 2012 20:49:54 +0100] rev 46340
separate orthogonal components
blanchet [Thu, 26 Jan 2012 20:49:54 +0100] rev 46339
generate left-to-right rewrite tag for combinator helpers for SPASS 3.8
blanchet [Thu, 26 Jan 2012 20:49:54 +0100] rev 46338
better handling of individual type for DFG format (SPASS)
bulwahn [Thu, 26 Jan 2012 12:04:05 +0100] rev 46337
adding quickcheck example with THE
bulwahn [Thu, 26 Jan 2012 12:03:35 +0100] rev 46336
evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.
bulwahn [Thu, 26 Jan 2012 10:59:47 +0100] rev 46335
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4
nipkow [Thu, 26 Jan 2012 09:52:47 +0100] rev 46334
tuned
bulwahn [Wed, 25 Jan 2012 16:07:48 +0100] rev 46333
adding very basic code generation to Wellfounded theory
bulwahn [Wed, 25 Jan 2012 16:07:41 +0100] rev 46332
removing dead code from Mutabelle; tuned
bulwahn [Wed, 25 Jan 2012 15:19:04 +0100] rev 46331
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn [Wed, 25 Jan 2012 09:50:34 +0100] rev 46330
merged
bulwahn [Wed, 25 Jan 2012 09:32:23 +0100] rev 46329
adding code equation for Collect on finite types
berghofe [Tue, 24 Jan 2012 16:00:51 +0100] rev 46328
Use lookup_size rather than Datatype.get_info in is_poly to avoid
incorrect results for datatypes on which no size function is defined
bulwahn [Tue, 24 Jan 2012 09:13:24 +0100] rev 46327
adding some rules to quickcheck's preprocessing
bulwahn [Tue, 24 Jan 2012 09:12:29 +0100] rev 46326
some more constants on mutabelle's blacklist
blanchet [Mon, 23 Jan 2012 17:40:32 +0100] rev 46325
implemented "tptp_refute" tool
blanchet [Mon, 23 Jan 2012 17:40:32 +0100] rev 46324
added problem importer
blanchet [Mon, 23 Jan 2012 17:40:32 +0100] rev 46323
imported patch ATP_Problem_Import.thy
blanchet [Mon, 23 Jan 2012 17:40:32 +0100] rev 46322
imported patch atp_problem_import.ML
blanchet [Mon, 23 Jan 2012 17:40:32 +0100] rev 46321
renamed theory exporter
blanchet [Mon, 23 Jan 2012 17:40:32 +0100] rev 46320
renamed two files to make room for a new file
blanchet [Mon, 23 Jan 2012 17:40:31 +0100] rev 46319
rebranded Nitrox, for more uniformity
blanchet [Mon, 23 Jan 2012 17:40:31 +0100] rev 46318
moved "nitrox" to TPTP
huffman [Mon, 23 Jan 2012 17:29:19 +0100] rev 46317
generalize type of List.listrel
bulwahn [Mon, 23 Jan 2012 15:23:02 +0100] rev 46316
support for Ex1 in quickcheck-narrowing
bulwahn [Mon, 23 Jan 2012 15:22:33 +0100] rev 46315
adding another internal constant to mutabelle's blacklust
bulwahn [Mon, 23 Jan 2012 14:08:55 +0100] rev 46314
adding some more forbidden constant names for the mutated conjecture generation
bulwahn [Mon, 23 Jan 2012 14:07:36 +0100] rev 46313
adding code generation for some list relations
bulwahn [Mon, 23 Jan 2012 14:06:19 +0100] rev 46312
adding fun_eq_iff to the preprocessing
bulwahn [Mon, 23 Jan 2012 14:00:52 +0100] rev 46311
random instance for sets
bulwahn [Mon, 23 Jan 2012 11:59:00 +0100] rev 46310
more configurations to mutabelle
bulwahn [Fri, 20 Jan 2012 09:28:54 +0100] rev 46309
catching code generation errors in quickcheck-narrowing
bulwahn [Fri, 20 Jan 2012 09:28:53 +0100] rev 46308
adding narrowing instance for sets
bulwahn [Fri, 20 Jan 2012 09:28:52 +0100] rev 46307
shortened definitions by adding some termify constants
bulwahn [Fri, 20 Jan 2012 09:28:51 +0100] rev 46306
tuned
bulwahn [Fri, 20 Jan 2012 09:28:50 +0100] rev 46305
adding check_all instance for sets; tuned
nipkow [Fri, 20 Jan 2012 08:24:51 +0100] rev 46304
tuned
nipkow [Fri, 20 Jan 2012 07:55:43 +0100] rev 46303
tuned
blanchet [Thu, 19 Jan 2012 21:37:12 +0100] rev 46302
minor edits in docs
blanchet [Thu, 19 Jan 2012 21:37:12 +0100] rev 46301
renamed "sound" option to "strict"
blanchet [Thu, 19 Jan 2012 21:37:12 +0100] rev 46300
updated Sledge docs some more
blanchet [Thu, 19 Jan 2012 21:37:12 +0100] rev 46299
more doc updates
blanchet [Thu, 19 Jan 2012 21:37:12 +0100] rev 46298
updated docs
blanchet [Thu, 19 Jan 2012 21:37:12 +0100] rev 46297
lower timeout for preplay, now that we have more preplay methods
blanchet [Thu, 19 Jan 2012 21:37:12 +0100] rev 46296
cleanly separate each Metis encoding
wenzelm [Thu, 09 Feb 2012 19:34:23 +0100] rev 46295
basic setup for equational reasoning;
updated rewrite_goals_tac and fold_goals_tac;
wenzelm [Tue, 07 Feb 2012 18:56:40 +0100] rev 46294
tuned;
wenzelm [Tue, 07 Feb 2012 18:51:22 +0100] rev 46293
updated examples for syntax translations;
wenzelm [Sun, 05 Feb 2012 21:00:38 +0100] rev 46292
updated section on raw syntax;
misc tuning;
wenzelm [Sun, 05 Feb 2012 18:11:19 +0100] rev 46291
updated section about syntax ambiguity;
wenzelm [Sat, 04 Feb 2012 18:33:04 +0100] rev 46290
updated/unified section on mixfix annotations;
wenzelm [Sat, 04 Feb 2012 16:08:19 +0100] rev 46289
tuned;
wenzelm [Sat, 04 Feb 2012 15:56:49 +0100] rev 46288
more on explicit notation;
wenzelm [Sat, 04 Feb 2012 15:44:50 +0100] rev 46287
more accurate Pure grammar;
wenzelm [Sat, 04 Feb 2012 14:25:14 +0100] rev 46286
more refs;
wenzelm [Sat, 04 Feb 2012 14:20:39 +0100] rev 46285
simplified mixfix (NB: infix is no longer required separately);
wenzelm [Thu, 02 Feb 2012 21:21:41 +0100] rev 46284
updated section on print modes;
wenzelm [Thu, 02 Feb 2012 20:26:44 +0100] rev 46283
misc tuning and reformatting;
more antiquotations;
wenzelm [Thu, 02 Feb 2012 18:11:42 +0100] rev 46282
clarified syntax section structure;
wenzelm [Thu, 02 Feb 2012 17:52:16 +0100] rev 46281
discontinued obscure history commands;
wenzelm [Thu, 02 Feb 2012 16:38:15 +0100] rev 46280
misc tuning and reformatting;
wenzelm [Thu, 02 Feb 2012 16:07:25 +0100] rev 46279
discontinued obscure history commands;
wenzelm [Sun, 29 Jan 2012 22:12:25 +0100] rev 46278
updated hint about asm_rl;
wenzelm [Sun, 29 Jan 2012 22:00:10 +0100] rev 46277
updated thin_tac;
wenzelm [Sun, 29 Jan 2012 21:40:29 +0100] rev 46276
updated distinct_subgoals_tac, flexflex_tac;
wenzelm [Sun, 29 Jan 2012 21:26:09 +0100] rev 46275
removed obscure material;
wenzelm [Sun, 29 Jan 2012 21:04:39 +0100] rev 46274
updated rotate_tac;
wenzelm [Fri, 27 Jan 2012 21:56:29 +0100] rev 46273
tuned;
wenzelm [Fri, 27 Jan 2012 21:48:40 +0100] rev 46272
updated citations;
wenzelm [Fri, 27 Jan 2012 21:29:37 +0100] rev 46271
updated subgoal_tac;
wenzelm [Thu, 26 Jan 2012 22:21:33 +0100] rev 46270
tuned sectioning;
wenzelm [Thu, 26 Jan 2012 22:16:45 +0100] rev 46269
updated "Control and search tacticals" (moved from ref to implementation);
discontinued odd trace flags that assume sequential TTY loop;
discontinued obscure DETERM_UNTIL_SOLVED;
discontinued obsolete chapter "Tacticals" (ref);
wenzelm [Thu, 26 Jan 2012 21:25:18 +0100] rev 46268
obsolete -- covered in implementation manual;
wenzelm [Thu, 26 Jan 2012 21:16:11 +0100] rev 46267
moved HEADGOAL;
added RANGE;
wenzelm [Thu, 26 Jan 2012 15:29:11 +0100] rev 46266
removed some obscure material;
misc tuning;
wenzelm [Thu, 26 Jan 2012 15:28:17 +0100] rev 46265
added SELECT_GOAL;
wenzelm [Thu, 26 Jan 2012 15:04:35 +0100] rev 46264
tuned;
wenzelm [Wed, 25 Jan 2012 22:01:15 +0100] rev 46263
updated "subgoal quantifiers";
wenzelm [Wed, 25 Jan 2012 21:14:00 +0100] rev 46262
tuned ML infixes;
wenzelm [Wed, 25 Jan 2012 21:10:54 +0100] rev 46261
document antiquotations for ML infix operators;
wenzelm [Wed, 25 Jan 2012 20:26:05 +0100] rev 46260
tuned;
wenzelm [Wed, 25 Jan 2012 19:04:38 +0100] rev 46259
updated repetition tacticals;
discontinued odd trace_REPEAT (assumes sequential TTY loop);
wenzelm [Wed, 25 Jan 2012 18:18:59 +0100] rev 46258
updated THEN, ORELSE, APPEND, and derivatives;
discontinued obscure INTLEAVE;
wenzelm [Wed, 25 Jan 2012 16:16:20 +0100] rev 46257
removed obscure/outdated material;
wenzelm [Wed, 25 Jan 2012 15:39:08 +0100] rev 46256
updated RSN, RL, RLN, MRS;
discontinued obscure MRL;
wenzelm [Wed, 25 Jan 2012 14:13:59 +0100] rev 46255
removed obscure/outdated material;
wenzelm [Wed, 25 Jan 2012 13:31:56 +0100] rev 46254
tuned;
wenzelm [Wed, 25 Jan 2012 13:24:57 +0100] rev 46253
more on Logic.all/mk_implies etc.;
wenzelm [Thu, 19 Jan 2012 16:16:13 +0100] rev 46252
reduce AFP test by many hours;
nipkow [Thu, 19 Jan 2012 09:51:42 +0100] rev 46251
added termination of narrowing
wenzelm [Wed, 18 Jan 2012 22:06:31 +0100] rev 46250
really need 64bit here;
prefer explicit version information for contrib;
nipkow [Wed, 18 Jan 2012 13:04:58 +0100] rev 46249
Added termination proof for widening
kleing [Wed, 18 Jan 2012 22:09:29 +1100] rev 46248
switch afp test to Darwin on macbroy2
nipkow [Wed, 18 Jan 2012 10:05:23 +0100] rev 46247
merged
nipkow [Wed, 18 Jan 2012 10:05:14 +0100] rev 46246
introduced commands over a set of vars
wenzelm [Wed, 18 Jan 2012 00:07:08 +0100] rev 46245
basic support for PIDE Scala programming, independently of the main Isabelle repository;
blanchet [Tue, 17 Jan 2012 18:25:36 +0100] rev 46244
fixed a bug introduced when porting functions to set -- extensionality on sets break the form of equations expected elsewhere by Nitpick
blanchet [Tue, 17 Jan 2012 18:25:36 +0100] rev 46243
updated message
blanchet [Tue, 17 Jan 2012 18:25:36 +0100] rev 46242
improve installation instructions
blanchet [Tue, 17 Jan 2012 18:25:36 +0100] rev 46241
allow use of proxy for remote SMT solver invocations, just like in the "remote_atp" script
huffman [Tue, 17 Jan 2012 16:30:54 +0100] rev 46240
factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
bulwahn [Tue, 17 Jan 2012 11:15:36 +0100] rev 46239
refreshing NEWS
bulwahn [Tue, 17 Jan 2012 10:45:42 +0100] rev 46238
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn [Tue, 17 Jan 2012 09:38:30 +0100] rev 46237
renamed theory AList to DAList
wenzelm [Mon, 16 Jan 2012 21:50:15 +0100] rev 46236
position constraints for numerals enable PIDE markup;
wenzelm [Mon, 16 Jan 2012 20:32:33 +0100] rev 46235
more careful cumulation of tooltips -- ensure uniform range;
wenzelm [Mon, 16 Jan 2012 13:19:44 +0100] rev 46234
tuned;
nipkow [Mon, 16 Jan 2012 07:55:10 +0100] rev 46233
tuned
nipkow [Mon, 16 Jan 2012 07:46:58 +0100] rev 46232
missing dependency
wenzelm [Sun, 15 Jan 2012 20:30:17 +0100] rev 46231
tuned example;
wenzelm [Sun, 15 Jan 2012 20:03:59 +0100] rev 46230
merged
wenzelm [Sun, 15 Jan 2012 19:55:31 +0100] rev 46229
back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
wenzelm [Sun, 15 Jan 2012 19:17:39 +0100] rev 46228
recovered outdated_color (cf. 4beb2f41ed93);
wenzelm [Sun, 15 Jan 2012 19:09:03 +0100] rev 46227
more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm [Sun, 15 Jan 2012 18:55:27 +0100] rev 46226
tuned proofs;
nipkow [Sun, 15 Jan 2012 17:27:46 +0100] rev 46225
tuned
wenzelm [Sun, 15 Jan 2012 14:55:30 +0100] rev 46224
tuned signature;
wenzelm [Sun, 15 Jan 2012 14:22:54 +0100] rev 46223
comments;
wenzelm [Sun, 15 Jan 2012 14:17:42 +0100] rev 46222
tuned proofs;