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. Regards, Jasmin _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
