| 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
|
| Mon, 12 Mar 2012 15:11:24 +0100 |
noschinl |
tuned simpset
|
file |
diff |
annotate
|
| Wed, 07 Mar 2012 21:34:36 +0100 |
haftmann |
tuned syntax; more candidates
|
file |
diff |
annotate
|
| Fri, 02 Mar 2012 21:45:45 +0100 |
haftmann |
more fundamental pred-to-set conversions for range and domain by means of inductive_set
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 19:34:52 +0100 |
haftmann |
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 21:44:12 +0100 |
haftmann |
restored accidental omission
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 21:26:28 +0100 |
haftmann |
tuned structure
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 20:43:33 +0100 |
haftmann |
tuned structure; dropped already existing syntax declarations
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 20:10:14 +0100 |
haftmann |
tuned syntax declarations; tuned structure
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 15:28:48 +0100 |
haftmann |
marked candidates for rule declarations
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 22:46:44 +0100 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 09:40:02 +0100 |
haftmann |
given up disfruitful branch
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 08:49:36 +0100 |
haftmann |
explicit remove of lattice notation
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 21:25:59 +0100 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 21:49:41 +0100 |
nipkow |
added "'a rel"
|
file |
diff |
annotate
|
| Sun, 01 Jan 2012 11:28:45 +0100 |
haftmann |
cleanup of code declarations
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:09 +0100 |
haftmann |
dropped obsolete code equation for Id
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 23:02:59 +0200 |
haftmann |
moved acyclic predicate up in hierarchy
|
file |
diff |
annotate
|