equal
deleted
inserted
replaced
135 infix 9 $$; |
135 infix 9 $$; |
136 infix 0 :== ===; |
136 infix 0 :== ===; |
137 infixr 0 ==>; |
137 infixr 0 ==>; |
138 |
138 |
139 val (op $$) = Term.list_comb; |
139 val (op $$) = Term.list_comb; |
140 val (op :==) = Logic.mk_defpair; |
140 val (op :==) = PrimitiveDefs.mk_defpair; |
141 val (op ===) = Trueprop o HOLogic.mk_eq; |
141 val (op ===) = Trueprop o HOLogic.mk_eq; |
142 val (op ==>) = Logic.mk_implies; |
142 val (op ==>) = Logic.mk_implies; |
143 |
143 |
144 (* morphisms *) |
144 (* morphisms *) |
145 |
145 |