this warning is hardly useful but produces noisy markers in the jedit interface
Description
Description
Details
Details
- Provenance
nipkow Authored on - Parents
- rISABELLE4cd4c204578c: undid 6d7b7a037e8d because it does not help but slows simplification down by up…
- Branches
- Unknown
- Tags