[isabelle-dev] Theory.thms_of ?

Walther Neuper wneuper at ist.tugraz.at
Mon Oct 11 18:05:00 CEST 2010


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 ...

Walther




More information about the isabelle-dev mailing list