2010-11-10 eliminated obsolete heading category -- superseded by heading_level;
wenzelm [Wed, 10 Nov 2010 15:47:56 +0100] rev 40459
eliminated obsolete heading category -- superseded by heading_level;
2010-11-10 treat main theory commands like headings, and nest anything else inside;
wenzelm [Wed, 10 Nov 2010 15:43:06 +0100] rev 40458
treat main theory commands like headings, and nest anything else inside;
2010-11-10 proper treatment of equal heading level;
wenzelm [Wed, 10 Nov 2010 15:42:20 +0100] rev 40457
proper treatment of equal heading level;
2010-11-10 added missing Keyword.THY_SCHEMATIC_GOAL;
wenzelm [Wed, 10 Nov 2010 15:41:29 +0100] rev 40456
added missing Keyword.THY_SCHEMATIC_GOAL; more keyword categories;
2010-11-10 default Sidekick parser based on section headings;
wenzelm [Wed, 10 Nov 2010 15:17:25 +0100] rev 40455
default Sidekick parser based on section headings;
2010-11-10 some support for nested source structure, based on section headings;
wenzelm [Wed, 10 Nov 2010 15:00:40 +0100] rev 40454
some support for nested source structure, based on section headings;
2010-11-10 tuned;
wenzelm [Wed, 10 Nov 2010 11:44:35 +0100] rev 40453
tuned;
2010-11-09 misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm [Tue, 09 Nov 2010 23:24:46 +0100] rev 40452
misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
2010-11-09 updated version;
wenzelm [Tue, 09 Nov 2010 22:37:10 +0100] rev 40451
updated version;
2010-11-09 private counter, to keep externalized ids a bit smaller;
wenzelm [Tue, 09 Nov 2010 21:52:05 +0100] rev 40450
private counter, to keep externalized ids a bit smaller;
2010-11-09 added general Synchronized.counter convenience;
wenzelm [Tue, 09 Nov 2010 21:44:19 +0100] rev 40449
added general Synchronized.counter convenience;
2010-11-09 explicitly identify forked/joined tasks;
wenzelm [Tue, 09 Nov 2010 21:13:06 +0100] rev 40448
explicitly identify forked/joined tasks;
2010-11-09 accomodate old manuals that include pdfsetup.sty without isabelle.sty;
wenzelm [Tue, 09 Nov 2010 11:27:58 +0100] rev 40447
accomodate old manuals that include pdfsetup.sty without isabelle.sty;
2010-11-09 merged
wenzelm [Tue, 09 Nov 2010 11:17:15 +0100] rev 40446
merged
2010-11-08 removed type-inference-like behaviour from relation_tac completely; tuned
krauss [Mon, 08 Nov 2010 23:02:20 +0100] rev 40445
removed type-inference-like behaviour from relation_tac completely; tuned
2010-11-08 avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);
wenzelm [Mon, 08 Nov 2010 20:55:27 +0100] rev 40444
avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);
2010-11-08 explicitly check uniqueness of symbol recoding;
wenzelm [Mon, 08 Nov 2010 20:50:56 +0100] rev 40443
explicitly check uniqueness of symbol recoding;
2010-11-08 more hints on building and running Isabelle/jEdit from command line;
wenzelm [Mon, 08 Nov 2010 17:44:47 +0100] rev 40442
more hints on building and running Isabelle/jEdit from command line;
2010-11-08 merged
wenzelm [Mon, 08 Nov 2010 14:41:11 +0100] rev 40441
merged
2010-11-08 merge
blanchet [Mon, 08 Nov 2010 14:33:54 +0100] rev 40440
merge
2010-11-08 reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
blanchet [Mon, 08 Nov 2010 14:33:30 +0100] rev 40439
reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving
2010-11-08 merged
huffman [Mon, 08 Nov 2010 05:07:18 -0800] rev 40438
merged
2010-11-06 merged
huffman [Sat, 06 Nov 2010 10:01:00 -0700] rev 40437
merged
2010-11-05 (infixl "<<" 55) -> (infix "<<" 50)
huffman [Fri, 05 Nov 2010 15:15:28 -0700] rev 40436
(infixl "<<" 55) -> (infix "<<" 50)
2010-11-04 simplify some proofs
huffman [Wed, 03 Nov 2010 17:22:25 -0700] rev 40435
simplify some proofs
2010-11-04 remove unnecessary stuff from Discrete.thy
huffman [Wed, 03 Nov 2010 17:06:21 -0700] rev 40434
remove unnecessary stuff from Discrete.thy
2010-11-03 remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
huffman [Wed, 03 Nov 2010 16:39:23 -0700] rev 40433
remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
2010-11-03 add lemma eq_imp_below
huffman [Wed, 03 Nov 2010 15:57:39 -0700] rev 40432
add lemma eq_imp_below
2010-11-03 discontinue a bunch of legacy theorem names
huffman [Wed, 03 Nov 2010 15:47:46 -0700] rev 40431
discontinue a bunch of legacy theorem names
2010-11-03 move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman [Wed, 03 Nov 2010 15:31:24 -0700] rev 40430
move a few admissibility lemmas into FOCUS/Stream_adm.thy
2010-11-03 simplify some proofs
huffman [Wed, 03 Nov 2010 15:03:16 -0700] rev 40429
simplify some proofs
2010-11-08 compile -- 7550b2cba1cb broke the build
blanchet [Mon, 08 Nov 2010 13:53:18 +0100] rev 40428
compile -- 7550b2cba1cb broke the build
2010-11-08 merge
blanchet [Mon, 08 Nov 2010 13:25:00 +0100] rev 40427
merge
2010-11-08 recognize Vampire error
blanchet [Mon, 08 Nov 2010 09:10:44 +0100] rev 40426
recognize Vampire error
2010-11-08 return the process return code along with the process outputs
boehmes [Mon, 08 Nov 2010 12:13:51 +0100] rev 40425
return the process return code along with the process outputs
2010-11-08 better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes [Mon, 08 Nov 2010 12:13:44 +0100] rev 40424
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
2010-11-08 merged
haftmann [Mon, 08 Nov 2010 11:49:28 +0100] rev 40423
merged
2010-11-08 corrected slip: must keep constant map, not type map; tuned code
haftmann [Mon, 08 Nov 2010 10:56:48 +0100] rev 40422
corrected slip: must keep constant map, not type map; tuned code
2010-11-08 constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann [Mon, 08 Nov 2010 10:43:24 +0100] rev 40421
constructors to datatypes in code_reflect can be globbed; dropped unused code
2010-11-08 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn [Mon, 08 Nov 2010 09:25:43 +0100] rev 40420
adding code and theory for smallvalue generators, but do not setup the interpretation yet
2010-11-08 make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
blanchet [Mon, 08 Nov 2010 02:33:48 +0100] rev 40419
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
2010-11-08 better detection of completely irrelevant facts
blanchet [Mon, 08 Nov 2010 02:32:27 +0100] rev 40418
better detection of completely irrelevant facts
2010-11-07 always use a hard timeout in Mirabelle
blanchet [Sun, 07 Nov 2010 18:19:04 +0100] rev 40417
always use a hard timeout in Mirabelle
2010-11-07 use "smt" (rather than "metis") to reconstruct SMT proofs
blanchet [Sun, 07 Nov 2010 18:15:13 +0100] rev 40416
use "smt" (rather than "metis") to reconstruct SMT proofs
2010-11-07 don't pass too many facts on the first iteration of the SMT solver
blanchet [Sun, 07 Nov 2010 18:03:24 +0100] rev 40415
don't pass too many facts on the first iteration of the SMT solver
2010-11-07 catch TimeOut exception
blanchet [Sun, 07 Nov 2010 18:02:02 +0100] rev 40414
catch TimeOut exception
2010-11-07 ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
blanchet [Sun, 07 Nov 2010 17:56:07 +0100] rev 40413
ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
2010-11-07 if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
blanchet [Sun, 07 Nov 2010 17:51:25 +0100] rev 40412
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
2010-11-07 removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
blanchet [Sun, 07 Nov 2010 13:29:59 +0100] rev 40411
removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
2010-11-06 make Nitpick datatype tests faster to make timeout less likely
blanchet [Sat, 06 Nov 2010 10:25:08 +0100] rev 40410
make Nitpick datatype tests faster to make timeout less likely
2010-11-06 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet [Sat, 06 Nov 2010 10:25:08 +0100] rev 40409
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
2010-11-06 always honor the max relevant constraint
blanchet [Sat, 06 Nov 2010 10:25:08 +0100] rev 40408
always honor the max relevant constraint
2010-11-08 more robust treatment of suppressed quotes concerning replacement text -- for improved copy/paste behaviour;
wenzelm [Mon, 08 Nov 2010 11:28:22 +0100] rev 40407
more robust treatment of suppressed quotes concerning replacement text -- for improved copy/paste behaviour;
2010-11-07 updated generated files;
wenzelm [Mon, 08 Nov 2010 00:00:47 +0100] rev 40406
updated generated files;
2010-11-07 tweaked pdf setup to allow modification of \pdfminorversion;
wenzelm [Sun, 07 Nov 2010 23:32:26 +0100] rev 40405
tweaked pdf setup to allow modification of \pdfminorversion;
2010-11-07 merged;
wenzelm [Sun, 07 Nov 2010 23:12:40 +0100] rev 40404
merged;
2010-11-07 updated generated files;
wenzelm [Sun, 07 Nov 2010 23:12:21 +0100] rev 40403
updated generated files;
2010-11-07 basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm [Sun, 07 Nov 2010 22:51:16 +0100] rev 40402
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
2010-11-07 updated generated file;
wenzelm [Sun, 07 Nov 2010 22:42:49 +0100] rev 40401
updated generated file;
2010-11-07 more literal appearance of antiqopen/antiqclose;
wenzelm [Sun, 07 Nov 2010 22:26:25 +0100] rev 40400
more literal appearance of antiqopen/antiqclose;
2010-11-07 'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);
wenzelm [Sun, 07 Nov 2010 16:39:03 +0100] rev 40399
'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);
2010-11-06 continue after failed commands;
wenzelm [Sat, 06 Nov 2010 20:59:59 +0100] rev 40398
continue after failed commands;
2010-11-06 added Keyword.is_heading (cf. Scala version);
wenzelm [Sat, 06 Nov 2010 20:18:06 +0100] rev 40397
added Keyword.is_heading (cf. Scala version); tuned;
2010-11-06 updated keywords;
wenzelm [Sat, 06 Nov 2010 19:37:31 +0100] rev 40396
updated keywords;
2010-11-06 mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
wenzelm [Sat, 06 Nov 2010 19:36:54 +0100] rev 40395
mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
2010-11-06 somewhat more uniform timing markup in ML vs. Scala;
wenzelm [Sat, 06 Nov 2010 18:10:35 +0100] rev 40394
somewhat more uniform timing markup in ML vs. Scala;
2010-11-06 somewhat more uniform timing in ML vs. Scala;
wenzelm [Sat, 06 Nov 2010 17:55:32 +0100] rev 40393
somewhat more uniform timing in ML vs. Scala;
2010-11-06 added Markup.Double, Markup.Double_Property;
wenzelm [Sat, 06 Nov 2010 16:53:07 +0100] rev 40392
added Markup.Double, Markup.Double_Property; tuned;
2010-11-06 explicit "timing" status for toplevel transactions;
wenzelm [Sat, 06 Nov 2010 16:31:35 +0100] rev 40391
explicit "timing" status for toplevel transactions;
2010-11-06 tuned;
wenzelm [Sat, 06 Nov 2010 16:03:49 +0100] rev 40390
tuned;
2010-11-06 tuned comments;
wenzelm [Sat, 06 Nov 2010 15:34:11 +0100] rev 40389
tuned comments;
2010-11-05 abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
krauss [Sat, 06 Nov 2010 00:10:32 +0100] rev 40388
abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
2010-11-05 moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
wenzelm [Fri, 05 Nov 2010 23:19:20 +0100] rev 40387
moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
2010-11-05 updated keywords;
wenzelm [Fri, 05 Nov 2010 22:03:57 +0100] rev 40386
updated keywords;
2010-11-05 reflect actual content of /home/isabelle/.html-data/cgi-bin/hgwebdir.cgi;
wenzelm [Fri, 05 Nov 2010 22:01:01 +0100] rev 40385
reflect actual content of /home/isabelle/.html-data/cgi-bin/hgwebdir.cgi;
2010-11-05 eliminated spurious "firstline" filters for improved display of Isabelle history logs: one item per line, without special headline;
wenzelm [Fri, 05 Nov 2010 21:53:25 +0100] rev 40384
eliminated spurious "firstline" filters for improved display of Isabelle history logs: one item per line, without special headline; more uniform shortlogentry and filelogentry;
2010-11-05 reflect actual content of /home/isabelle-repository/hgweb-templates/isabelle by krauss;
wenzelm [Fri, 05 Nov 2010 21:48:48 +0100] rev 40383
reflect actual content of /home/isabelle-repository/hgweb-templates/isabelle by krauss;
2010-11-05 obsolete -- python installation on www4 is not modified (despite remaining "firstline" in graph and syndication views);
wenzelm [Fri, 05 Nov 2010 21:42:32 +0100] rev 40382
obsolete -- python installation on www4 is not modified (despite remaining "firstline" in graph and syndication views);
2010-11-05 explicit indication of some remaining violations of the Isabelle/ML interrupt model;
wenzelm [Fri, 05 Nov 2010 19:47:20 +0100] rev 40381
explicit indication of some remaining violations of the Isabelle/ML interrupt model;
2010-11-05 updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;
wenzelm [Fri, 05 Nov 2010 19:39:25 +0100] rev 40380
updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;
2010-11-05 proper spelling;
wenzelm [Fri, 05 Nov 2010 19:22:04 +0100] rev 40379
proper spelling; proper format;
2010-11-05 merged
hoelzl [Fri, 05 Nov 2010 15:09:55 +0100] rev 40378
merged
2010-11-05 Extend convex analysis by Bogdan Grechuk
hoelzl [Fri, 05 Nov 2010 14:17:18 +0100] rev 40377
Extend convex analysis by Bogdan Grechuk
2010-11-05 merged
blanchet [Fri, 05 Nov 2010 14:36:17 +0100] rev 40376
merged
2010-11-05 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
blanchet [Fri, 05 Nov 2010 09:49:03 +0100] rev 40375
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
2010-11-05 make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information
blanchet [Fri, 05 Nov 2010 09:05:22 +0100] rev 40374
make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information
2010-11-04 pass proper type to SMT_Builtin.is_builtin
blanchet [Thu, 04 Nov 2010 15:31:26 +0100] rev 40373
pass proper type to SMT_Builtin.is_builtin
2010-11-04 remove " s" suffix since seconds are now implicit
blanchet [Thu, 04 Nov 2010 15:30:48 +0100] rev 40372
remove " s" suffix since seconds are now implicit
2010-11-04 ignore facts with only theory constants in them
blanchet [Thu, 04 Nov 2010 14:59:44 +0100] rev 40371
ignore facts with only theory constants in them
2010-11-04 cosmetics
blanchet [Thu, 04 Nov 2010 14:59:44 +0100] rev 40370
cosmetics
2010-11-04 use the SMT integration's official list of built-ins
blanchet [Thu, 04 Nov 2010 14:59:44 +0100] rev 40369
use the SMT integration's official list of built-ins
2010-11-05 added class relation group_add < cancel_semigroup_add
haftmann [Fri, 05 Nov 2010 14:10:41 +0100] rev 40368
added class relation group_add < cancel_semigroup_add
2010-11-05 merged
bulwahn [Fri, 05 Nov 2010 09:07:14 +0100] rev 40367
merged
2010-11-05 changing timeout to real value; handling Interrupt and Timeout more like nitpick does
bulwahn [Fri, 05 Nov 2010 08:16:35 +0100] rev 40366
changing timeout to real value; handling Interrupt and Timeout more like nitpick does
2010-11-05 added two lemmas about injectivity of concat to the list theory
bulwahn [Fri, 05 Nov 2010 08:16:34 +0100] rev 40365
added two lemmas about injectivity of concat to the list theory
2010-11-05 adding documentation of some quickcheck options
bulwahn [Fri, 05 Nov 2010 08:16:31 +0100] rev 40364
adding documentation of some quickcheck options
2010-11-05 merged
haftmann [Fri, 05 Nov 2010 08:28:57 +0100] rev 40363
merged
2010-11-04 Code.check_const etc.: reject too specific types
haftmann [Thu, 04 Nov 2010 17:27:38 +0100] rev 40362
Code.check_const etc.: reject too specific types
2010-11-04 corrected quoting
haftmann [Thu, 04 Nov 2010 17:27:37 +0100] rev 40361
corrected quoting
2010-11-04 added lemma length_alloc
haftmann [Thu, 04 Nov 2010 17:27:37 +0100] rev 40360
added lemma length_alloc
2010-11-04 dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
haftmann [Thu, 04 Nov 2010 13:42:36 +0100] rev 40359
dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
2010-11-04 added note on countable types
haftmann [Thu, 04 Nov 2010 13:42:36 +0100] rev 40358
added note on countable types
2010-11-04 simulate more closely the behaviour of the tactic
boehmes [Thu, 04 Nov 2010 18:01:55 +0100] rev 40357
simulate more closely the behaviour of the tactic
2010-11-04 merged
wenzelm [Thu, 04 Nov 2010 17:17:21 +0100] rev 40356
merged
2010-11-04 merged
haftmann [Thu, 04 Nov 2010 13:37:11 +0100] rev 40355
merged
2010-11-04 merged
haftmann [Thu, 04 Nov 2010 09:54:16 +0100] rev 40354
merged
2010-11-03 dropped debug message
haftmann [Wed, 03 Nov 2010 14:14:06 +0100] rev 40353
dropped debug message
2010-11-03 more precise text
haftmann [Wed, 03 Nov 2010 14:14:06 +0100] rev 40352
more precise text
2010-11-03 SMLdummy target
haftmann [Wed, 03 Nov 2010 14:14:05 +0100] rev 40351
SMLdummy target
2010-11-03 fixed typos
haftmann [Wed, 03 Nov 2010 14:14:05 +0100] rev 40350
fixed typos
2010-11-03 moved theory Quicksort from Library/ to ex/
haftmann [Wed, 03 Nov 2010 12:20:33 +0100] rev 40349
moved theory Quicksort from Library/ to ex/
2010-11-03 Theory Multiset provides stable quicksort implementation of sort_key.
haftmann [Wed, 03 Nov 2010 12:20:33 +0100] rev 40348
Theory Multiset provides stable quicksort implementation of sort_key.
2010-11-03 added code lemmas for stable parametrized quicksort
haftmann [Wed, 03 Nov 2010 12:15:47 +0100] rev 40347
added code lemmas for stable parametrized quicksort
2010-11-03 tuned proof
haftmann [Wed, 03 Nov 2010 11:50:29 +0100] rev 40346
tuned proof
2010-11-04 moved file in makefile to reflect actual dependencies
blanchet [Thu, 04 Nov 2010 09:53:23 +0100] rev 40345
moved file in makefile to reflect actual dependencies
2010-11-03 give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet [Wed, 03 Nov 2010 23:01:30 +0100] rev 40344
give E one more second, to prevent cases where it finds a proof but has no time to print it
2010-11-03 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
blanchet [Wed, 03 Nov 2010 22:51:32 +0100] rev 40343
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages; updated docs
2010-11-03 don't be overly verbose in Sledgehammer's minimizer
blanchet [Wed, 03 Nov 2010 22:33:23 +0100] rev 40342
don't be overly verbose in Sledgehammer's minimizer
2010-11-03 standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet [Wed, 03 Nov 2010 22:26:53 +0100] rev 40341
standardize on seconds for Nitpick and Sledgehammer timeouts
2010-11-03 cleaned up
nipkow [Wed, 03 Nov 2010 20:19:24 +0100] rev 40340
cleaned up
(0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip