Mon, 22 Nov 2010 09:19:34 +0100 tuned
haftmann [Mon, 22 Nov 2010 09:19:34 +0100] rev 40630
tuned
Mon, 22 Nov 2010 09:18:25 +0100 tuned
haftmann [Mon, 22 Nov 2010 09:18:25 +0100] rev 40629
tuned
Sat, 20 Nov 2010 01:07:16 +0100 updated explode vs. raw_explode;
wenzelm [Sat, 20 Nov 2010 01:07:16 +0100] rev 40628
updated explode vs. raw_explode;
Sat, 20 Nov 2010 00:53:26 +0100 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm [Sat, 20 Nov 2010 00:53:26 +0100] rev 40627
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
Fri, 19 Nov 2010 23:48:07 +0100 total Symbol.explode (cf. 1050315f6ee2);
wenzelm [Fri, 19 Nov 2010 23:48:07 +0100] rev 40626
total Symbol.explode (cf. 1050315f6ee2);
Fri, 19 Nov 2010 21:14:12 +0100 do not export Thy_Load.required, to avoid confusion about the interface;
wenzelm [Fri, 19 Nov 2010 21:14:12 +0100] rev 40625
do not export Thy_Load.required, to avoid confusion about the interface;
Fri, 19 Nov 2010 09:07:23 -0800 merged
huffman [Fri, 19 Nov 2010 09:07:23 -0800] rev 40624
merged
Wed, 17 Nov 2010 16:13:33 -0800 declare adm_chfin [simp]
huffman [Wed, 17 Nov 2010 16:13:33 -0800] rev 40623
declare adm_chfin [simp]
Wed, 17 Nov 2010 16:05:18 -0800 add lemma cont_fun; remove unused lemma monofun_app
huffman [Wed, 17 Nov 2010 16:05:18 -0800] rev 40622
add lemma cont_fun; remove unused lemma monofun_app
Wed, 17 Nov 2010 12:19:19 -0800 accumulated NEWS updates for HOLCF
huffman [Wed, 17 Nov 2010 12:19:19 -0800] rev 40621
accumulated NEWS updates for HOLCF
Wed, 17 Nov 2010 11:39:44 -0800 section -> subsection
huffman [Wed, 17 Nov 2010 11:39:44 -0800] rev 40620
section -> subsection
Wed, 17 Nov 2010 11:07:02 -0800 add lemma adm_prod_case
huffman [Wed, 17 Nov 2010 11:07:02 -0800] rev 40619
add lemma adm_prod_case
Fri, 19 Nov 2010 14:59:11 +0000 merged
paulson [Fri, 19 Nov 2010 14:59:11 +0000] rev 40618
merged
Fri, 19 Nov 2010 14:58:49 +0000 First-order pattern matching: catch a rogue exception (differing numbers of arguments)
paulson [Fri, 19 Nov 2010 14:58:49 +0000] rev 40617
First-order pattern matching: catch a rogue exception (differing numbers of arguments)
Fri, 19 Nov 2010 14:35:58 +0100 eval simp rules for predicate type, simplify primitive proofs
haftmann [Fri, 19 Nov 2010 14:35:58 +0100] rev 40616
eval simp rules for predicate type, simplify primitive proofs
Fri, 19 Nov 2010 11:44:46 +0100 generalized type
haftmann [Fri, 19 Nov 2010 11:44:46 +0100] rev 40615
generalized type
Fri, 19 Nov 2010 10:37:06 +0100 made smlnj happy
haftmann [Fri, 19 Nov 2010 10:37:06 +0100] rev 40614
made smlnj happy
Fri, 19 Nov 2010 10:04:08 +0100 merged
haftmann [Fri, 19 Nov 2010 10:04:08 +0100] rev 40613
merged
Thu, 18 Nov 2010 18:53:36 +0100 proper qualification needed due to shadowing on theory merge
haftmann [Thu, 18 Nov 2010 18:53:36 +0100] rev 40612
proper qualification needed due to shadowing on theory merge
Thu, 18 Nov 2010 17:06:02 +0100 more appropriate name for property
haftmann [Thu, 18 Nov 2010 17:06:02 +0100] rev 40611
more appropriate name for property
Thu, 18 Nov 2010 17:01:16 +0100 mapper for sum type
haftmann [Thu, 18 Nov 2010 17:01:16 +0100] rev 40610
mapper for sum type
Thu, 18 Nov 2010 17:01:16 +0100 mapper for option type
haftmann [Thu, 18 Nov 2010 17:01:16 +0100] rev 40609
mapper for option type
Thu, 18 Nov 2010 17:01:16 +0100 mapper for list type; map_pair replaces prod_fun
haftmann [Thu, 18 Nov 2010 17:01:16 +0100] rev 40608
mapper for list type; map_pair replaces prod_fun
Thu, 18 Nov 2010 17:01:16 +0100 map_pair replaces prod_fun
haftmann [Thu, 18 Nov 2010 17:01:16 +0100] rev 40607
map_pair replaces prod_fun
Thu, 18 Nov 2010 17:01:16 +0100 mapper for mulitset type
haftmann [Thu, 18 Nov 2010 17:01:16 +0100] rev 40606
mapper for mulitset type
Thu, 18 Nov 2010 17:01:16 +0100 mapper for mapping type
haftmann [Thu, 18 Nov 2010 17:01:16 +0100] rev 40605
mapper for mapping type
Thu, 18 Nov 2010 17:01:15 +0100 mapper for fset type
haftmann [Thu, 18 Nov 2010 17:01:15 +0100] rev 40604
mapper for fset type
Thu, 18 Nov 2010 17:01:15 +0100 mapper for dlist type
haftmann [Thu, 18 Nov 2010 17:01:15 +0100] rev 40603
mapper for dlist type
Thu, 18 Nov 2010 17:01:15 +0100 map_fun combinator in theory Fun
haftmann [Thu, 18 Nov 2010 17:01:15 +0100] rev 40602
map_fun combinator in theory Fun
Thu, 18 Nov 2010 22:34:32 +0100 some updates after 2 years of Mercurial usage;
wenzelm [Thu, 18 Nov 2010 22:34:32 +0100] rev 40601
some updates after 2 years of Mercurial usage;
Thu, 18 Nov 2010 18:12:03 +0100 mention Sledgehammer with SMT
blanchet [Thu, 18 Nov 2010 18:12:03 +0100] rev 40600
mention Sledgehammer with SMT
Thu, 18 Nov 2010 18:09:08 +0100 enabled SMT solver in Sledgehammer by default
blanchet [Thu, 18 Nov 2010 18:09:08 +0100] rev 40599
enabled SMT solver in Sledgehammer by default
Thu, 18 Nov 2010 12:37:30 +0100 merged
haftmann [Thu, 18 Nov 2010 12:37:30 +0100] rev 40598
merged
Thu, 18 Nov 2010 10:59:42 +0100 keep variables bound
haftmann [Thu, 18 Nov 2010 10:59:42 +0100] rev 40597
keep variables bound
Thu, 18 Nov 2010 10:52:38 +0100 remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem
blanchet [Thu, 18 Nov 2010 10:52:38 +0100] rev 40596
remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem
Wed, 17 Nov 2010 23:20:26 +0100 merged
haftmann [Wed, 17 Nov 2010 23:20:26 +0100] rev 40595
merged
Wed, 17 Nov 2010 17:27:25 +0100 infer variances of user-given mapper operation; proper thm storing
haftmann [Wed, 17 Nov 2010 17:27:25 +0100] rev 40594
infer variances of user-given mapper operation; proper thm storing
Wed, 17 Nov 2010 21:35:23 +0100 code eqn for slice was missing; redefined splice with fun
nipkow [Wed, 17 Nov 2010 21:35:23 +0100] rev 40593
code eqn for slice was missing; redefined splice with fun
Wed, 17 Nov 2010 08:47:58 -0800 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman [Wed, 17 Nov 2010 08:47:58 -0800] rev 40592
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
Wed, 17 Nov 2010 06:49:23 -0800 merged
huffman [Wed, 17 Nov 2010 06:49:23 -0800] rev 40591
merged
Tue, 16 Nov 2010 16:36:57 -0800 typedef (open) unit
huffman [Tue, 16 Nov 2010 16:36:57 -0800] rev 40590
typedef (open) unit
Tue, 16 Nov 2010 13:37:17 -0800 add bind_bind rules for powerdomains
huffman [Tue, 16 Nov 2010 13:37:17 -0800] rev 40589
add bind_bind rules for powerdomains
Wed, 17 Nov 2010 13:50:02 +0100 merged
wenzelm [Wed, 17 Nov 2010 13:50:02 +0100] rev 40588
merged
Wed, 17 Nov 2010 12:24:58 +0100 emerging Isar command interface
haftmann [Wed, 17 Nov 2010 12:24:58 +0100] rev 40587
emerging Isar command interface
Wed, 17 Nov 2010 11:38:47 +0100 fixed typo
haftmann [Wed, 17 Nov 2010 11:38:47 +0100] rev 40586
fixed typo
Wed, 17 Nov 2010 11:38:46 +0100 updated keywords
haftmann [Wed, 17 Nov 2010 11:38:46 +0100] rev 40585
updated keywords
Wed, 17 Nov 2010 11:27:48 +0100 ML signature interface
haftmann [Wed, 17 Nov 2010 11:27:48 +0100] rev 40584
ML signature interface
Wed, 17 Nov 2010 11:26:39 +0100 stub for Isar command interface
haftmann [Wed, 17 Nov 2010 11:26:39 +0100] rev 40583
stub for Isar command interface
Wed, 17 Nov 2010 11:09:18 +0100 module for functorial mappers
haftmann [Wed, 17 Nov 2010 11:09:18 +0100] rev 40582
module for functorial mappers
Wed, 17 Nov 2010 13:39:30 +0100 merged
wenzelm [Wed, 17 Nov 2010 13:39:30 +0100] rev 40581
merged
Wed, 17 Nov 2010 09:22:23 +0100 require the b2i file ending in the boogie_open command (for consistency with the theory header)
boehmes [Wed, 17 Nov 2010 09:22:23 +0100] rev 40580
require the b2i file ending in the boogie_open command (for consistency with the theory header)
Wed, 17 Nov 2010 08:14:56 +0100 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes [Wed, 17 Nov 2010 08:14:56 +0100] rev 40579
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
Wed, 17 Nov 2010 08:14:55 +0100 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes [Wed, 17 Nov 2010 08:14:55 +0100] rev 40578
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
Tue, 16 Nov 2010 12:08:28 -0800 add lemmas about powerdomains
huffman [Tue, 16 Nov 2010 12:08:28 -0800] rev 40577
add lemmas about powerdomains
Tue, 16 Nov 2010 11:57:10 -0800 declare {upper,lower,convex}_pd_induct as default induction rules
huffman [Tue, 16 Nov 2010 11:57:10 -0800] rev 40576
declare {upper,lower,convex}_pd_induct as default induction rules
Tue, 16 Nov 2010 11:50:05 -0800 rename 'repdef' to 'domaindef'
huffman [Tue, 16 Nov 2010 11:50:05 -0800] rev 40575
rename 'repdef' to 'domaindef'
Wed, 17 Nov 2010 13:38:53 +0100 refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;
wenzelm [Wed, 17 Nov 2010 13:38:53 +0100] rev 40574
refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;
Wed, 17 Nov 2010 11:24:07 +0100 less parentheses, cf. Session.welcome;
wenzelm [Wed, 17 Nov 2010 11:24:07 +0100] rev 40573
less parentheses, cf. Session.welcome;
Tue, 16 Nov 2010 22:40:45 +0100 avoid spam;
wenzelm [Tue, 16 Nov 2010 22:40:45 +0100] rev 40572
avoid spam;
Tue, 16 Nov 2010 22:13:54 +0100 more robust determination of java executable;
wenzelm [Tue, 16 Nov 2010 22:13:54 +0100] rev 40571
more robust determination of java executable;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip