Changes by: Kamal Aboul-Hosn (kamal at cs.cornell.edu)
Date: 2003-12-29 09:43:14 -0800 (Mon, 29 Dec 2003)
Revision: 5218
Log message:

      Added reduce to appropriate rules.  The list is maintained in the file
      I use to convert from KAT-ML and adds the automatically in the conversion.
      Also started to define Hoare rules in the standard way with ifs and whiles
      and to let MetaPRL do the conversion on its own.
      

Changes  Path
+20 -1 metaprl/theories/kat/kat_MSDriver.ml
+123 -9 metaprl/theories/kat/kat_ax.ml
+17 -9 metaprl/theories/kat/kat_bool.ml
+7 -1 metaprl/theories/kat/kat_denest.ml
+26 -183 metaprl/theories/kat/kat_hoare.ml
+28 -5 metaprl/theories/kat/kat_std.ml
+11 -0 metaprl/theories/kat/kat_terms.ml