Tactic#showToBeginner theorems, intermed.
authorwneuper
Thu, 21 Feb 2008 11:50:28 +0100
changeset 3892c9fd1b03e0c3
parent 3891 7fbe7b1efeea
child 3893 c6e6c271ee07
Tactic#showToBeginner theorems, intermed.
src/java/isac/util/tactics/Tactic.java
     1.1 --- a/src/java/isac/util/tactics/Tactic.java	Thu Feb 21 09:39:15 2008 +0100
     1.2 +++ b/src/java/isac/util/tactics/Tactic.java	Thu Feb 21 11:50:28 2008 +0100
     1.3 @@ -6,10 +6,11 @@
     1.4  
     1.5  import isac.util.formulae.CalcElement;
     1.6  import isac.util.formulae.CalcFormula;
     1.7 +import isac.util.formulae.Formula;
     1.8  
     1.9  /**
    1.10 - * @author Alan Krempler (method stubs)
    1.11 - * FIXME.WN0504 redesign this class wrt. inherited elements
    1.12 + * @author Alan Krempler (method stubs) FIXME.WN0504 redesign this class wrt.
    1.13 + *         inherited elements
    1.14   */
    1.15  public class Tactic extends CalcElement {
    1.16  
    1.17 @@ -27,39 +28,75 @@
    1.18          return "";
    1.19      }
    1.20  
    1.21 -    //WN0504 put down in inheritance (valid only for some tacs)
    1.22 +    /**
    1.23 +     * WN0504 put down in inheritance (valid only for some tacs)
    1.24 +     * 
    1.25 +     * WN080221 questionable if this should be due to inheritance
    1.26 +     * 
    1.27 +     * @see isac.util.tactics.Tactic#showToBeginner()
    1.28 +     */
    1.29      public String getTheoremName() {
    1.30          return "";
    1.31      }
    1.32  
    1.33 -    //WN0504 put down in inheritance (valid only for some tacs)
    1.34 +    /**
    1.35 +     * WN0504 put down in inheritance (valid only for some tacs)
    1.36 +     * 
    1.37 +     * WN080221 questionable if this should be due to inheritance ...
    1.38 +     * 
    1.39 +     * @see isac.util.tactics.Tactic#showToBeginner()
    1.40 +     */
    1.41      public String getTheoremDescription() {
    1.42          return "";
    1.43      }
    1.44  
    1.45 -    //WN0504 put down in inheritance (valid only for some tacs)
    1.46 -    public CalcFormula getTheoremSymbolic() {
    1.47 -        CalcFormula dummy;
    1.48 -        dummy = new CalcFormula();
    1.49 +    /**
    1.50 +     * show the Formula contained in this Tactic
    1.51 +     * 
    1.52 +     * WN0504 put down in inheritance (valid only for some tacs)
    1.53 +     * 
    1.54 +     * WN080221 ...questionable if this should be due to inheritance ...
    1.55 +     * 
    1.56 +     * @see isac.util.tactics.Tactic#showToBeginner()
    1.57 +     */
    1.58 +    public Formula getTheoremSymbolic() {
    1.59 +        Formula dummy;
    1.60 +        dummy = new Formula();
    1.61          return dummy;
    1.62      }
    1.63  
    1.64 -    //WN0504 put down in inheritance (valid only for some tacs)
    1.65 -    public CalcFormula getTheoremInstantiated(CalcFormula formula) {
    1.66 -        CalcFormula dummy;
    1.67 -        dummy = new CalcFormula();
    1.68 +    /**
    1.69 +     * show the Formula contained in this Tactic instantiated with form (makes
    1.70 +     * only sense, if this can be done within isacs java-part)
    1.71 +     * 
    1.72 +     * WN0504 put down in inheritance (valid only for some tacs)
    1.73 +     * 
    1.74 +     * WN080221 ...questionable if this should be due to inheritance ...
    1.75 +     * 
    1.76 +     * @see isac.util.tactics.Tactic#showToBeginner()
    1.77 +     */
    1.78 +    public Formula getTheoremInstantiated(Formula form) {
    1.79 +        Formula dummy;
    1.80 +        dummy = new Formula();
    1.81          return dummy;
    1.82      }
    1.83  
    1.84 -    //WN0504 put down within inheritance tree (valid only for some tacs)
    1.85 -    // itself and selected by passing an integer
    1.86 -    public CalcFormula makeFillFormula(CalcFormula formula, String pattern) {
    1.87 -        CalcFormula dummy;
    1.88 -        dummy = new CalcFormula();
    1.89 +    /**
    1.90 +     * WN0504 put down in inheritance (valid only for some tacs) itself and
    1.91 +     * selected by passing an integer
    1.92 +     * 
    1.93 +     * WN080221 questionable if this should be due to inheritance ...
    1.94 +     * 
    1.95 +     * @see isac.util.tactics.Tactic#showToBeginner()
    1.96 +     */
    1.97 +    // 
    1.98 +    public Formula makeFillFormula(Formula formula, String pattern) {
    1.99 +        Formula dummy;
   1.100 +        dummy = new Formula();
   1.101          return dummy;
   1.102      }
   1.103  
   1.104 -    /*
   1.105 +    /**
   1.106       * (non-Javadoc)
   1.107       * 
   1.108       * @see isac.util.CalcElement#getText()
   1.109 @@ -68,6 +105,17 @@
   1.110          return null;
   1.111      }
   1.112  
   1.113 +    /**
   1.114 +     * show the tactic to a beginner in a most simple form
   1.115 +     * 
   1.116 +     * WN080221 only shown like ..
   1.117 +     * 
   1.118 +     * @see isac.util.tactics.Tactic#getTheoremSymbolic()
   1.119 +     */
   1.120 +    public String showToBeginner() {
   1.121 +        return this.toSMLString();
   1.122 +    }
   1.123 +
   1.124      /*
   1.125       * (non-Javadoc)
   1.126       *