src/Pure/Isar/local_defs.ML

 
 
 
 (** defived definitions **)
 
-(* transformation rules *)
+(* transformation via rewrite rules *)
 
 structure Rules = Generic_Data
 (
   type T = thm list;
   val empty = [];
   val extend = I;
   val merge = Thm.merge_thms;
 );
 
 fun print_rules ctxt =
-  Pretty.writeln (Pretty.big_list "definitional transformations:"
+  Pretty.writeln (Pretty.big_list "definitional rewrite rules:"
     (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
 
 val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
 val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);