| changeset 1129 | 9a86f0ef6503 |
| parent 1128 | 17ca92ab4660 |
| child 1137 | 36d596cb63a2 |
| 1128:17ca92ab4660 | 1129:9a86f0ef6503 |
|---|---|
796 |
796 |
797 attribute_setup quot_lifted = |
797 attribute_setup quot_lifted = |
798 {* Scan.succeed Quotient_Tacs.lifted_attrib *} |
798 {* Scan.succeed Quotient_Tacs.lifted_attrib *} |
799 {* lifts theorems to quotient types *} |
799 {* lifts theorems to quotient types *} |
800 |
800 |
801 no_notation |
|
802 rel_conj (infixr "OOO" 75) and |
|
803 fun_map (infixr "--->" 55) and |
|
804 fun_rel (infixr "===>" 55) |
|
805 |
|
801 end |
806 end |
802 |
807 |