src/Pure/Isar/find_theorems.ML
changeset 18325 2d504ea54e5b
parent 18184 43c4589a9a78
child 18939 18e2a2676d80
equal deleted inserted replaced
18324:d1c4b1112e33 18325:2d504ea54e5b
   234 
   234 
   235 
   235 
   236 (* print_theorems *)
   236 (* print_theorems *)
   237 
   237 
   238 fun find_thms ctxt spec =
   238 fun find_thms ctxt spec =
   239   (PureThy.thms_containing (ProofContext.theory_of ctxt) spec @
   239   (PureThy.thms_containing (ProofContext.theory_of ctxt) spec
   240     ProofContext.lthms_containing ctxt spec)
   240     |> map PureThy.selections
   241   |> map PureThy.selections |> List.concat;
   241     |> List.concat) @
       
   242   (ProofContext.lthms_containing ctxt spec
       
   243     |> map PureThy.selections
       
   244     |> List.concat
       
   245     |> gen_distinct (fn ((r1, th1), (r2, th2)) =>
       
   246         r1 = r2 andalso Drule.eq_thm_prop (th1, th2)));
   242 
   247 
   243 fun print_theorems ctxt opt_goal opt_limit raw_criteria =
   248 fun print_theorems ctxt opt_goal opt_limit raw_criteria =
   244   let
   249   let
   245     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
   250     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
   246     val filters = map (filter_criterion ctxt opt_goal) criteria;
   251     val filters = map (filter_criterion ctxt opt_goal) criteria;