Definitions clarification

In the `defs.txt` there are terms not defined neither on the article nor the references I searched. Could you please explain the syntaxis of this:

```
on_circle x o a
x : x o a
o a = diff o a
x : cong o x o a
circle o o a
```

What is diff there, and what is the : doing? And the final circle, that is not the syntax of circle(O, A, B, C) that means center O and passes through A, B, C. How many interpretations are for the circle predicate?

Thanks in advance.