| Thu, 29 May 2014 11:11:22 +0200 |
nipkow |
typo
|
file |
diff |
annotate
|
| Tue, 29 Apr 2014 16:02:02 +0200 |
wenzelm |
prefer plain ASCII / latex over not-so-universal Unicode;
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 14:53:22 +0200 |
haftmann |
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP)
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 11:27:36 +0200 |
haftmann |
more operations and lemmas
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 18:47:22 +0100 |
haftmann |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
killed a few 'metis' calls
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Tue, 21 Jan 2014 13:21:55 +0100 |
traytel |
removed theory dependency of BNF_LFP on Datatype
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 20:21:12 +0100 |
blanchet |
move BNF_LFP up the dependency chain
|
file |
diff |
annotate
|
| Fri, 29 Nov 2013 08:26:45 +0100 |
traytel |
set_comprehension_pointfree simproc causes to many surprises if enabled by default
|
file |
diff |
annotate
|
| Thu, 21 Nov 2013 21:33:34 +0100 |
blanchet |
rationalize imports
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 19:28:51 +0100 |
hoelzl |
countability of the image of a reflexive transitive closure
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:20 +0200 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
| Tue, 17 Sep 2013 08:42:51 +0200 |
nipkow |
added lemmas and made concerse executable
|
file |
diff |
annotate
|
| Sun, 28 Jul 2013 12:59:59 +0200 |
traytel |
more converse(p) theorems; tuned proofs;
|
file |
diff |
annotate
|
| Thu, 25 Jul 2013 12:25:07 +0200 |
traytel |
two useful relation theorems
|
file |
diff |
annotate
|
| Wed, 19 Jun 2013 10:06:24 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Fri, 07 Dec 2012 15:53:28 +0100 |
nipkow |
corrected nonsensical associativity of `` and dvd
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 13:55:39 +0200 |
kuncar |
more relation operations expressed by Finite_Set.fold
|
file |
diff |
annotate
|
| Thu, 12 Jul 2012 16:22:33 +0200 |
bulwahn |
a first guess to avoid the Codegenerator_Test to loop infinitely
|
file |
diff |
annotate
|
| Wed, 16 May 2012 19:17:20 +0200 |
kuncar |
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 11:01:15 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 17:45:06 +0900 |
griff |
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 17:26:30 +0900 |
griff |
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
|
file |
diff |
annotate
|
| Thu, 05 Apr 2012 15:23:26 +0200 |
huffman |
define reflp directly, in the manner of symp and transp
|
file |
diff |
annotate
|
| Thu, 22 Mar 2012 18:54:39 +0100 |
haftmann |
fixed typo
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 11:35:18 +0100 |
haftmann |
spelt out missing colemmas
|
file |
diff |
annotate
|
| Sat, 17 Mar 2012 08:00:18 +0100 |
haftmann |
generalized INF_INT_eq, SUP_UN_eq
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 21:41:11 +0100 |
noschinl |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 15:12:22 +0100 |
noschinl |
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
|
file |
diff |
annotate
|