Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2002-08-09 08:59:20 -0700 (Fri, 09 Aug 2002)
Revision: 3780
Log message:

      Removed the special-case handling for axioms (rules without arguments and without
      assumptions).
      
      *** WARNING ***
      
      This commit breaks binary compatibility! Before doing "cvs update":
      - make sure all your proof modifications are exported into .prla files
      After "cvs update":
      - do "make clean" and erase the theories/*/*.prlb files.
      

Changes  Path
+0 -8 metaprl/editor/ml/shell.ml
+1 -3 metaprl/editor/ml/shell_package.ml
+0 -34 metaprl/editor/ml/shell_rule.ml
+0 -6 metaprl/editor/ml/shell_rule.mli
+3 -67 metaprl/filter/base/filter_prog.ml
+6 -88 metaprl/filter/base/filter_summary.ml
+0 -5 metaprl/filter/base/filter_summary.mli
+0 -7 metaprl/filter/base/filter_type.ml
+6 -23 metaprl/filter/filter/filter_parse.ml
+1 -1 metaprl/mk/preface
+13 -190 metaprl/refiner/refiner/refine.ml
+5 -32 metaprl/refiner/refsig/refine_sig.ml
+1 -1 metaprl/theories/fol/fol_false.mli
+3 -9 metaprl/theories/tactic/summary.ml
+0 -1 metaprl/theories/tactic/summary.mli