| Thu, 12 Jun 2014 18:47:27 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 18:47:16 +0200 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 17:02:03 +0200 |
blanchet |
reintroduced vital 'Thm.transfer'
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
reduces Sledgehammer dependencies
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 21:15:57 +0200 |
blanchet |
changed syntax of map: and rel: arguments to BNF-based datatypes
|
file |
diff |
annotate
|
| Tue, 10 Jun 2014 12:16:22 +0200 |
blanchet |
use 'where' clause for selector default value syntax
|
file |
diff |
annotate
|
| Mon, 09 Jun 2014 16:08:30 +0200 |
nipkow |
added List.union
|
file |
diff |
annotate
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
tuned whitespace, to make datatype definitions slightly less intimidating
|
file |
diff |
annotate
|
| Mon, 26 May 2014 16:32:55 +0200 |
blanchet |
got rid of '=:' squiggly
|
file |
diff |
annotate
|
| Wed, 14 May 2014 11:33:38 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Tue, 29 Apr 2014 16:02:02 +0200 |
wenzelm |
prefer plain ASCII / latex over not-so-universal Unicode;
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
move size hooks together, with new one preceding old one and sharing same theory data
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 11:27:36 +0200 |
haftmann |
more operations and lemmas
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:54 +0200 |
kuncar |
make list_all an abbreviation of pred_list - prevent duplication
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:32 +0200 |
kuncar |
simplify and fix theories thanks to 356a5efdb278
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:15 +0200 |
kuncar |
abstract Domainp in relator_domain rules => more natural statement of the rule
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:15 +0200 |
kuncar |
more appropriate name (Lifting.invariant -> eq_onp)
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:14 +0200 |
kuncar |
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 11:42:32 +0100 |
wenzelm |
more qualified names;
|
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
|
| Sun, 16 Mar 2014 18:09:04 +0100 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
killed a few 'metis' calls
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:29:18 +0100 |
blanchet |
renamed 'prod_rel' to 'rel_prod'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 14:57:14 +0100 |
blanchet |
renamed 'set_rel' to 'rel_set'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:36:48 +0100 |
blanchet |
renamed 'map_pair' to 'map_prod'
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 17:54:52 +0100 |
traytel |
load Metis a little later
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 18:09:37 +0100 |
nipkow |
added function "List.extract"
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 16:32:37 +0100 |
blanchet |
merged 'List.set' with BNF-generated 'set'
|
file |
diff |
annotate
|