| 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
|
| Thu, 13 Mar 2014 13:18:14 +0100 |
blanchet |
renamed (hardly used) 'prod_pred' and 'option_pred' to 'pred_prod' and 'pred_option'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:03:49 +0100 |
kuncar |
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 21:33:28 +0100 |
blanchet |
folded 'rel_option' into 'option_rel'
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
merged 'Option.map' and 'Option.map_option'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
|
file |
diff |
annotate
|
| Fri, 24 Jan 2014 11:51:45 +0100 |
blanchet |
killed 'More_BNFs' by moving its various bits where they (now) belong
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 23:43:42 +0100 |
blanchet |
technical import to avoid infamous 'duplicate Option.size' error at merge time in 'List.thy'
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 23:34:26 +0100 |
blanchet |
swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 18:22:55 +0200 |
traytel |
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 15:59:22 +0200 |
kuncar |
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
|
file |
diff |
annotate
|