src/Tools/GraphBrowser/graphbrowser/ParseError.java
author haftmann
Tue, 01 Jul 2025 20:51:26 +0200
changeset 82801 c8d92d4ced73
parent 74015 12b1f4649ab1
permissions -rw-r--r--
isabelle regenerate_cooper

package isabelle.graphbrowser;

class ParseError extends Exception {
	public ParseError(String s) { super(s); }
}