Re: [isabelle] Multiset ordering vs. subset syntax



Hi all,

> I am not sure whether it would be best to do the swap in one step.

Actually, Florianâs email made me rethink about this, and maybe as many as three steps will be necessary (leading us to Isabelle2016-1 or Isabelle2017):

1. Rename <# etc. to #<# (or whatever odd syntax).
2. Rename < and \<subset> to <# and \<subset>#.
3. Rename #<# to <.

My goal is to maximize the number of cases where changes trigger clear errors when processing theories, and minimize subtle change of semantics. Even in a theorem prover, semantic changes can be difficult to debug. Combining steps 2 and 3 would lead to some confusion â a term like âA < Bâ would suddenly change semantics, without giving an immediate error.

Anyway, we will see. For the moment, if there are no voices against my implementing step 1, I will go ahead (e.g. next week).

Thanks to all for your feedback!

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.