wenzelm [Mon, 15 Nov 2010 17:39:23 +0100] rev 40546
eliminated old-style sed in favour of builtin regex matching;
wenzelm [Mon, 15 Nov 2010 17:14:43 +0100] rev 40545
more robust treatment of spaces in file names;
wenzelm [Mon, 15 Nov 2010 15:41:58 +0100] rev 40544
tuned error messages;
wenzelm [Mon, 15 Nov 2010 14:59:53 +0100] rev 40543
merged
haftmann [Mon, 15 Nov 2010 14:59:21 +0100] rev 40542
re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)
haftmann [Mon, 15 Nov 2010 14:14:38 +0100] rev 40541
re-generalized type of prod_rel (accident from 2989f9f3aa10)
boehmes [Mon, 15 Nov 2010 00:20:36 +0100] rev 40540
formal dependency on b2i files
boehmes [Sun, 14 Nov 2010 23:55:25 +0100] rev 40539
merged
boehmes [Fri, 12 Nov 2010 17:28:43 +0100] rev 40538
check the return code of the SMT solver and raise an exception if the prover failed
wenzelm [Sun, 14 Nov 2010 17:33:28 +0100] rev 40537
updated README;
wenzelm [Sun, 14 Nov 2010 15:25:01 +0100] rev 40536
tuned;
wenzelm [Sun, 14 Nov 2010 15:21:49 +0100] rev 40535
cover 'write' as primitive proof command;
wenzelm [Sun, 14 Nov 2010 14:05:08 +0100] rev 40534
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
wenzelm [Sat, 13 Nov 2010 22:33:07 +0100] rev 40533
somewhat adhoc replacement for 'thus' and 'hence';
complete words as short as 2 characters, e.g. "Un";
wenzelm [Sat, 13 Nov 2010 21:46:24 +0100] rev 40532
always print state of proof commands (notably "qed" etc.);
wenzelm [Sat, 13 Nov 2010 21:01:03 +0100] rev 40531
simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;
wenzelm [Sat, 13 Nov 2010 20:49:02 +0100] rev 40530
tuned message;
wenzelm [Sat, 13 Nov 2010 20:20:05 +0100] rev 40529
proper escape in regex;
wenzelm [Sat, 13 Nov 2010 20:13:35 +0100] rev 40528
report malformed symbols;
wenzelm [Sat, 13 Nov 2010 20:06:52 +0100] rev 40527
qualified Symbol_Pos.symbol;
wenzelm [Sat, 13 Nov 2010 19:55:45 +0100] rev 40526
total Symbol.source;
wenzelm [Sat, 13 Nov 2010 19:47:23 +0100] rev 40525
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm [Sat, 13 Nov 2010 19:27:41 +0100] rev 40524
treat Unicode "replacement character" (i.e. decoding error) is malformed;
wenzelm [Sat, 13 Nov 2010 19:21:53 +0100] rev 40523
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
allow malformed symbols inside quoted material, comments etc. -- for improved user experience with incremental re-parsing;
refined treatment of malformed surrogates (Scala);
wenzelm [Sat, 13 Nov 2010 16:46:00 +0100] rev 40522
tuned;
wenzelm [Sat, 13 Nov 2010 12:32:21 +0100] rev 40521
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
wenzelm [Sat, 13 Nov 2010 11:41:02 +0100] rev 40520
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
wenzelm [Sat, 13 Nov 2010 00:24:41 +0100] rev 40519
updated README;
wenzelm [Fri, 12 Nov 2010 21:37:01 +0100] rev 40518
defensive defaults for more robust experience for new users;
wenzelm [Fri, 12 Nov 2010 17:44:03 +0100] rev 40517
merged
boehmes [Fri, 12 Nov 2010 15:56:11 +0100] rev 40516
preliminary support for newer versions of Z3
boehmes [Fri, 12 Nov 2010 15:56:10 +0100] rev 40515
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes [Fri, 12 Nov 2010 15:56:08 +0100] rev 40514
let the theory formally depend on the Boogie output
boehmes [Fri, 12 Nov 2010 15:56:07 +0100] rev 40513
look for certificates relative to the theory
boehmes [Fri, 12 Nov 2010 15:56:06 +0100] rev 40512
dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT
huffman [Fri, 12 Nov 2010 06:11:29 -0800] rev 40511
merged
huffman [Fri, 12 Nov 2010 06:05:26 -0800] rev 40510
update Theory.requires with new theory name
wenzelm [Fri, 12 Nov 2010 14:51:28 +0100] rev 40509
tuned signatures;
wenzelm [Fri, 12 Nov 2010 14:06:37 +0100] rev 40508
never open Unsynchronized;
wenzelm [Fri, 12 Nov 2010 12:57:02 +0100] rev 40507
merged
huffman [Wed, 10 Nov 2010 18:45:48 -0800] rev 40506
section headings
huffman [Wed, 10 Nov 2010 18:37:11 -0800] rev 40505
reorder chapters for generated document
huffman [Wed, 10 Nov 2010 18:30:17 -0800] rev 40504
merge Representable.thy into Domain.thy
huffman [Wed, 10 Nov 2010 18:15:21 -0800] rev 40503
move stuff from Domain.thy to Domain_Aux.thy
huffman [Wed, 10 Nov 2010 17:56:08 -0800] rev 40502
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman [Wed, 10 Nov 2010 14:59:52 -0800] rev 40501
allow unpointed lazy arguments for definitional domain package
huffman [Wed, 10 Nov 2010 14:20:47 -0800] rev 40500
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman [Wed, 10 Nov 2010 13:22:39 -0800] rev 40499
merged
huffman [Wed, 10 Nov 2010 13:08:42 -0800] rev 40498
removed unused lemma chain_mono2
huffman [Wed, 10 Nov 2010 11:42:35 -0800] rev 40497
rename class 'bifinite' to 'domain'
huffman [Wed, 10 Nov 2010 09:59:08 -0800] rev 40496
instance sum :: (predomain, predomain) predomain
huffman [Wed, 10 Nov 2010 09:52:50 -0800] rev 40495
configure sum type for fixrec
huffman [Wed, 10 Nov 2010 08:18:32 -0800] rev 40494
add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)
huffman [Wed, 10 Nov 2010 06:02:37 -0800] rev 40493
instance prod :: (predomain, predomain) predomain
huffman [Tue, 09 Nov 2010 19:37:11 -0800] rev 40492
adapt isodefl proof script to unpointed types
huffman [Tue, 09 Nov 2010 16:37:13 -0800] rev 40491
add 'predomain' class: unpointed version of bifinite
huffman [Tue, 09 Nov 2010 08:41:36 -0800] rev 40490
add bifiniteness check for domain_isomorphism command
huffman [Tue, 09 Nov 2010 05:23:34 -0800] rev 40489
implement map_of_typ using Pattern.rewrite_term
huffman [Tue, 09 Nov 2010 04:47:46 -0800] rev 40488
avoid using stale theory
huffman [Mon, 08 Nov 2010 15:13:45 -0800] rev 40487
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
huffman [Mon, 08 Nov 2010 14:36:17 -0800] rev 40486
add function the_sort
huffman [Mon, 08 Nov 2010 14:09:07 -0800] rev 40485
refactor tmp_thy code
huffman [Mon, 08 Nov 2010 06:58:09 -0800] rev 40484
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
wenzelm [Fri, 12 Nov 2010 11:36:01 +0100] rev 40483
treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;
wenzelm [Fri, 12 Nov 2010 10:58:09 +0100] rev 40482
Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation;
wenzelm [Thu, 11 Nov 2010 19:58:07 +0100] rev 40481
more precise treatment of deleted nodes;
wenzelm [Thu, 11 Nov 2010 18:55:17 +0100] rev 40480
tuned error message;
wenzelm [Thu, 11 Nov 2010 17:07:05 +0100] rev 40479
unified type Document.Edit;
wenzelm [Thu, 11 Nov 2010 16:48:46 +0100] rev 40478
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
Document_Model.pending_edits: more robust treatment of init, including buffer reload event (jEdit 4.3.2 produces malformed remove/insert that lacks the last character);
tuned;
wenzelm [Thu, 11 Nov 2010 13:23:39 +0100] rev 40477
tuned;
wenzelm [Thu, 11 Nov 2010 13:07:41 +0100] rev 40476
reduced danger of line breaks within minipage;
wenzelm [Wed, 10 Nov 2010 20:43:22 +0100] rev 40475
Sidekick block asset: show first line only;
wenzelm [Wed, 10 Nov 2010 20:21:55 +0100] rev 40474
added buffer_text convenience, with explicit locking;
wenzelm [Wed, 10 Nov 2010 17:53:41 +0100] rev 40473
use official/portable Multithreading.max_threads_value, which is also subject to user preferences (NB: Thread.numProcessors is apt to lead to surprises like very high numbers for systems with hyperthreading);
wenzelm [Wed, 10 Nov 2010 16:05:15 +0100] rev 40472
merged
blanchet [Wed, 10 Nov 2010 09:03:07 +0100] rev 40471
make SML/NJ happy
haftmann [Tue, 09 Nov 2010 16:18:40 +0100] rev 40470
merged
haftmann [Tue, 09 Nov 2010 14:02:14 +0100] rev 40469
slightly changed fun_map_def
haftmann [Tue, 09 Nov 2010 14:02:14 +0100] rev 40468
fun_rel_def is no simp rule by default
haftmann [Tue, 09 Nov 2010 14:02:13 +0100] rev 40467
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann [Tue, 09 Nov 2010 14:02:13 +0100] rev 40466
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann [Tue, 09 Nov 2010 14:02:13 +0100] rev 40465
more appropriate specification packages; fun_rel_def is no simp rule by default
haftmann [Tue, 09 Nov 2010 14:02:12 +0100] rev 40464
type annotations in specifications; fun_rel_def is no simp rule by default
haftmann [Tue, 09 Nov 2010 14:02:12 +0100] rev 40463
fun_rel_def is no simp rule by default
paulson [Tue, 09 Nov 2010 14:00:10 +0000] rev 40462
merged
paulson [Tue, 09 Nov 2010 13:59:37 +0000] rev 40461
tidied using metis
wenzelm [Wed, 10 Nov 2010 15:59:23 +0100] rev 40460
manage folding via sidekick by default;
wenzelm [Wed, 10 Nov 2010 15:47:56 +0100] rev 40459
eliminated obsolete heading category -- superseded by heading_level;
wenzelm [Wed, 10 Nov 2010 15:43:06 +0100] rev 40458
treat main theory commands like headings, and nest anything else inside;
wenzelm [Wed, 10 Nov 2010 15:42:20 +0100] rev 40457
proper treatment of equal heading level;
wenzelm [Wed, 10 Nov 2010 15:41:29 +0100] rev 40456
added missing Keyword.THY_SCHEMATIC_GOAL;
more keyword categories;
wenzelm [Wed, 10 Nov 2010 15:17:25 +0100] rev 40455
default Sidekick parser 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;
wenzelm [Wed, 10 Nov 2010 11:44:35 +0100] rev 40453
tuned;
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);
wenzelm [Tue, 09 Nov 2010 22:37:10 +0100] rev 40451
updated version;
wenzelm [Tue, 09 Nov 2010 21:52:05 +0100] rev 40450
private counter, to keep externalized ids a bit smaller;
wenzelm [Tue, 09 Nov 2010 21:44:19 +0100] rev 40449
added general Synchronized.counter convenience;
wenzelm [Tue, 09 Nov 2010 21:13:06 +0100] rev 40448
explicitly identify forked/joined tasks;
wenzelm [Tue, 09 Nov 2010 11:27:58 +0100] rev 40447
accomodate old manuals that include pdfsetup.sty without isabelle.sty;
wenzelm [Tue, 09 Nov 2010 11:17:15 +0100] rev 40446
merged
krauss [Mon, 08 Nov 2010 23:02:20 +0100] rev 40445
removed type-inference-like behaviour from relation_tac completely; tuned
wenzelm [Mon, 08 Nov 2010 20:55:27 +0100] rev 40444
avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8);
wenzelm [Mon, 08 Nov 2010 20:50:56 +0100] rev 40443
explicitly check uniqueness of symbol recoding;
wenzelm [Mon, 08 Nov 2010 17:44:47 +0100] rev 40442
more hints on building and running Isabelle/jEdit from command line;
wenzelm [Mon, 08 Nov 2010 14:41:11 +0100] rev 40441
merged
blanchet [Mon, 08 Nov 2010 14:33:54 +0100] rev 40440
merge
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
huffman [Mon, 08 Nov 2010 05:07:18 -0800] rev 40438
merged
huffman [Sat, 06 Nov 2010 10:01:00 -0700] rev 40437
merged
huffman [Fri, 05 Nov 2010 15:15:28 -0700] rev 40436
(infixl "<<" 55) -> (infix "<<" 50)
huffman [Wed, 03 Nov 2010 17:22:25 -0700] rev 40435
simplify some proofs
huffman [Wed, 03 Nov 2010 17:06:21 -0700] rev 40434
remove unnecessary stuff from Discrete.thy
huffman [Wed, 03 Nov 2010 16:39:23 -0700] rev 40433
remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
huffman [Wed, 03 Nov 2010 15:57:39 -0700] rev 40432
add lemma eq_imp_below
huffman [Wed, 03 Nov 2010 15:47:46 -0700] rev 40431
discontinue a bunch of legacy theorem names
huffman [Wed, 03 Nov 2010 15:31:24 -0700] rev 40430
move a few admissibility lemmas into FOCUS/Stream_adm.thy
huffman [Wed, 03 Nov 2010 15:03:16 -0700] rev 40429
simplify some proofs
blanchet [Mon, 08 Nov 2010 13:53:18 +0100] rev 40428
compile -- 7550b2cba1cb broke the build
blanchet [Mon, 08 Nov 2010 13:25:00 +0100] rev 40427
merge