equal
deleted
inserted
replaced
373 |
373 |
374 |
374 |
375 (* print_theorems *) |
375 (* print_theorems *) |
376 |
376 |
377 fun all_facts_of ctxt = |
377 fun all_facts_of ctxt = |
378 maps Facts.selections |
378 let |
379 (Facts.dest_static [] (PureThy.facts_of (ProofContext.theory_of ctxt)) @ |
379 fun visible_facts facttab = |
380 Facts.dest_static [] (ProofContext.facts_of ctxt)); |
380 Facts.dest_static [] facttab |
|
381 |> filter_out (Facts.is_concealed facttab o #1) |
|
382 in |
|
383 maps Facts.selections |
|
384 (visible_facts (PureThy.facts_of (ProofContext.theory_of ctxt)) @ |
|
385 visible_facts (ProofContext.facts_of ctxt)) |
|
386 end; |
381 |
387 |
382 val limit = Unsynchronized.ref 40; |
388 val limit = Unsynchronized.ref 40; |
383 |
389 |
384 fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = |
390 fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = |
385 let |
391 let |