[isabelle-dev] Theory.thms_of ?

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Tue Oct 12 03:52:06 CEST 2010

Hi Walther,

> how can one get all theorems proven in a theory, i.e. some function * with signature
>    'val *: theory -> thm list
> The only related functions I find are 'Theory.axioms_of' (which ignores theorems) and  'PureThy.get_thms' (which requires as an argument, e.g. 'PureThy.get_thms (theory "Rings") "divide_zero_left";' I want to have as a result ...

Global_Theory.all_thms_of has a slightly different signature but is probably what you want.



More information about the isabelle-dev mailing list