src/Provers/simplifier.ML

 val delN = "del";
 val onlyN = "only";
 val no_asmN = "no_asm";
 val no_asm_useN = "no_asm_use";
 val no_asm_simpN = "no_asm_simp";
+val asm_lrN = "asm_lr";
 
 val simp_attr =
  (Attrib.add_del_args simp_add_global simp_del_global,
   Attrib.add_del_args simp_add_local simp_del_local);
 

 
 val simp_options =
  (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
   Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
   Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
+  Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
   Scan.succeed asm_full_simp_tac);
 
 val cong_modifiers =
  [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier),
   Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local),