src/Provers/hypsubst.ML
changeset 12377 c1e3e7d3f469
parent 12262 11ff5f47df6e
child 13604 57bfacbbaeda
equal deleted inserted replaced
12376:480303e3fa08 12377:c1e3e7d3f469
   259 val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac);
   259 val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac);
   260 val hyp_subst_meth =
   260 val hyp_subst_meth =
   261   Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac));
   261   Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac));
   262 
   262 
   263 
   263 
   264 (* attributes *)
       
   265 
       
   266 fun symmetric_rule thm =
       
   267   thm RS Drule.symmetric_thm handle THM _ =>
       
   268   thm RS Data.sym handle THM _ => error "Failed to apply symmetry of == or =";
       
   269 
       
   270 fun gen_symmetric x = Drule.rule_attribute (K symmetric_rule);
       
   271 
       
   272 
       
   273 (* theory setup *)
   264 (* theory setup *)
   274 
   265 
   275 val hypsubst_setup =
   266 val hypsubst_setup =
   276  [Method.add_methods
   267  [Method.add_methods
   277   [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
   268   [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
   278    ("subst", subst_meth, "substitution")],
   269    ("subst", subst_meth, "substitution")]];
   279   Attrib.add_attributes
       
   280   [("symmetric", (gen_symmetric, gen_symmetric), "resolution with symmetry of == or =")]];
       
   281 
   270 
   282 end;
   271 end;