lib/browser/GraphBrowser/ParseError.java
author kleing
Wed, 20 Jul 2005 07:40:23 +0200
changeset 16895 df67fc190e06
parent 13973 9170772bf420
permissions -rw-r--r--
Sort search results in order of relevance, where relevance = a) better if 0 premises for intro or 1 premise for elim/dest rules b) better if substitution size wrt to current goal is smaller Only applies to intro, dest, elim, and simp (contributed by Rafal Kolanski, NICTA)

package GraphBrowser;

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