Session Auto2_HOL
View
theory dependencies
View
document
View
outline
Theories
Auto2_Setup
File ‹util.ML›
File ‹util_base.ML›
File ‹util_logic.ML›
File ‹box_id.ML›
File ‹consts.ML›
File ‹property.ML›
File ‹wellform.ML›
File ‹wfterm.ML›
File ‹rewrite.ML›
File ‹propertydata.ML›
File ‹matcher.ML›
File ‹items.ML›
File ‹wfdata.ML›
File ‹auto2_data.ML›
File ‹status.ML›
File ‹normalize.ML›
File ‹proofsteps.ML›
File ‹auto2_state.ML›
File ‹logic_steps.ML›
File ‹auto2.ML›
File ‹auto2_outer.ML›
File ‹auto2_setup.ML›
Auto2_HOL_Extra_Setup
File ‹acdata.ML›
File ‹ac_steps.ML›
File ‹unfolding.ML›
File ‹induct_outer.ML›
File ‹extra_hol.ML›
File ‹auto2_hol_extra_setup.ML›
HOL_Base
Auto2_HOL_Setup
File ‹auto2_hol_util_base.ML›
Logic_Thms
Order_Thms
File ‹util_arith.ML›
Arith_Thms
File ‹arith.ML›
File ‹order.ML›
File ‹order_test.ML›
File ‹nat_sub.ML›
File ‹nat_sub_test.ML›
HOL-Library.Cancellation
File ‹Cancellation/cancel.ML›
File ‹Cancellation/cancel_data.ML›
File ‹Cancellation/cancel_simprocs.ML›
HOL-Library.Multiset
File ‹multiset_simprocs.ML›
Set_Thms
Lists_Thms
File ‹list_ac.ML›
File ‹list_ac_test.ML›
Auto2_Main
Auto2_Test
File ‹util_test.ML›
File ‹rewrite_test.ML›
File ‹matcher_test.ML›
File ‹normalize_test.ML›
File ‹logic_steps_test.ML›
File ‹acdata_test.ML›
Pelletier
Primes_Ex