In the attached development, the interactive proof for thm1/S-THM will cause the following exception when trying XD
java.lang.IllegalArgumentException: Trying to add an invalid self-referring type: S
This bug is reported by J-R. Abrial via email.
The matching facilities are now reimplemented using ISpecialization which is the proper way for instantiate types. This fix will be available in the next release of the Theory plug-in.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
The matching facilities are now reimplemented using ISpecialization which is the proper way for instantiate types. This fix will be available in the next release of the Theory plug-in.
This bug has been fixed and can't be reproduced with the latest release.