TODO 2002-05-26 - PDF Generation: \qed must be on the right edge - PDF Generation: proof line references go to the first proof line! error! - PDF Generation & HTML Generation: Used by list at end - Make Text only Paragraphs - is SubstLine ok? if a free variable is changed into a bound one this must be an error! one has to look at RenameBoundVariable RenameFreeVariable and ReplacePredicat - proof lines with line number? A: yes we must change that - write module transformation functions: - expand all proofs that reference internal sentence labels - expand all proofs that reference sentence labels - new operator "DECLARE" for declaring a keyword that could be used further on, "ABBREVIATION" is an implicit declaration. Every mathematical operator and every proof rule must be declared before you could use it. Sometimes a declaration could have arguments: eg.: the rules of de Morgan require a reference to a proposition that proofs -(A & B) <=> -A v -B A: DECLARE for rules implemented, for operators we decided against doing it - is getPartFormulaSize() neccessary, why don't use instance of Formula? - allow no Counter with number==0 - make TestXMLrunnable in normal enviornment - generate basic classes or methods with generators: write down parsing rules and parse them to generate code - allow different proofs: this means also use of different imports why that? allow only different proofs! - check entries of AbbrevitationList: do they use anything after (or in) current entry (check for recursivness) - make new Abbrevitation for operators with variable argument number - rename: AND -> LAND, OR -> LOR - make new operators AND, OR with variable argument numbers - more construction tests for proofs and their subarguments - new tests for package tests - new unit tests - check all "TODO" s in source code - new "definition" for predicate constants -> logic package - adapt checkit doclet - document PackageTest (and parameter -t) - PackageTest: some more test files for Exceptions - check error messages - Input: add new Constructor for InputStream - check: toString() must be final, if used in hashCode() - set certain modifer to "protected" in certain methods of Argument (e.g. matchEnumerator)