equal
deleted
inserted
replaced
771 fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y; |
771 fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y; |
772 *} |
772 *} |
773 attach (test) {* |
773 attach (test) {* |
774 fun gen_id_42 aG bG i = (aG i, bG i); |
774 fun gen_id_42 aG bG i = (aG i, bG i); |
775 *} |
775 *} |
|
776 |
|
777 consts_code |
|
778 "Pair" ("(_,/ _)") |
|
779 "fst" ("fst") |
|
780 "snd" ("snd") |
776 |
781 |
777 code_alias |
782 code_alias |
778 "*" "Product_Type.*" |
783 "*" "Product_Type.*" |
779 "Pair" "Product_Type.Pair" |
784 "Pair" "Product_Type.Pair" |
780 "fst" "Product_Type.fst" |
785 "fst" "Product_Type.fst" |