equal
deleted
inserted
replaced
767 treated automatically, but usually need to be expanded by hand, |
767 treated automatically, but usually need to be expanded by hand, |
768 using the collective fact @{text "t.defs"}. |
768 using the collective fact @{text "t.defs"}. |
769 |
769 |
770 \end{enumerate} |
770 \end{enumerate} |
771 *} |
771 *} |
|
772 |
|
773 |
|
774 subsubsection {* Examples *} |
|
775 |
|
776 text {* See @{file "~~/src/HOL/ex/Records.thy"}, for example. *} |
772 |
777 |
773 |
778 |
774 section {* Adhoc tuples *} |
779 section {* Adhoc tuples *} |
775 |
780 |
776 text {* |
781 text {* |