src/CCL/Wfd.thy
changeset 32282 853ef99c04cc
parent 32211 752dbe71cc89
child 32283 3bebc195c124
equal deleted inserted replaced
32281:750101435f60 32282:853ef99c04cc
   496 
   496 
   497 local
   497 local
   498   structure Data = Named_Thms(val name = "eval" val description = "evaluation rules");
   498   structure Data = Named_Thms(val name = "eval" val description = "evaluation rules");
   499 in
   499 in
   500 
   500 
   501 fun eval_tac ctxt ths i =
   501 fun eval_tac ths =
   502   DEPTH_SOLVE_1 (resolve_tac (ths @ Data.get ctxt) i ORELSE assume_tac i);
   502   FOCUS_PREMS (fn {context, prems, ...} =>
       
   503     DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1));
   503 
   504 
   504 val eval_setup =
   505 val eval_setup =
   505   Data.setup #>
   506   Data.setup #>
   506   Method.setup @{binding eval}
   507   Method.setup @{binding eval}
   507     (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ctxt ths)))
   508     (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt)))
   508     "evaluation";
   509     "evaluation";
   509 
   510 
   510 end;
   511 end;
   511 
   512 
   512 *}
   513 *}