lib/browser/GraphBrowser/ParseError.java
author huffman
Fri, 20 Apr 2012 15:34:33 +0200
changeset 47626 f7b1034cb9ce
parent 13973 9170772bf420
permissions -rw-r--r--
move definition of set_rel into Library/Quotient_Set.thy

package GraphBrowser;

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