equal
deleted
inserted
replaced
260 infix 9 $$; |
260 infix 9 $$; |
261 infix 0 :== ===; |
261 infix 0 :== ===; |
262 infixr 0 ==>; |
262 infixr 0 ==>; |
263 |
263 |
264 val op $$ = Term.list_comb; |
264 val op $$ = Term.list_comb; |
265 val op :== = PrimitiveDefs.mk_defpair; |
265 val op :== = Primitive_Defs.mk_defpair; |
266 val op === = Trueprop o HOLogic.mk_eq; |
266 val op === = Trueprop o HOLogic.mk_eq; |
267 val op ==> = Logic.mk_implies; |
267 val op ==> = Logic.mk_implies; |
268 |
268 |
269 |
269 |
270 (* constructor *) |
270 (* constructor *) |