Defdsl

Created by: SimonGuilloud

New DSL to make definitions: val orderedPair = DEF (x, y) --> unorderedPair(unorderedPair(x, x), unorderedPair(x, y)) val intersection = DEF (x, y) --> The (z, forall(a, in(a,z) <=> (in(a, x) /\ in(a,y)))) (intersectionThm)

Idea is that the proof is not done directly in the definition, but in a theorem first that is then used to make the definition. I think it's cleaner.

New error and error printing for definitions

Additionally, small corrections in the kernel and some new utilities. Make printing of file path in errors work with windows systems ()