src/HOL/HOL.thy
changeset 31299 0c5baf034d0e
parent 31173 bbe9e29b9672
child 31804 627d142fce19
equal deleted inserted replaced
31298:5e6b2b23701a 31299:0c5baf034d0e
    29   "~~/src/Tools/induct.ML"
    29   "~~/src/Tools/induct.ML"
    30   ("~~/src/Tools/induct_tacs.ML")
    30   ("~~/src/Tools/induct_tacs.ML")
    31   ("Tools/recfun_codegen.ML")
    31   ("Tools/recfun_codegen.ML")
    32 begin
    32 begin
    33 
    33 
    34 setup {* Intuitionistic.method_setup "iprover" *}
    34 setup {* Intuitionistic.method_setup @{binding iprover} *}
    35 
    35 
    36 
    36 
    37 subsection {* Primitive logic *}
    37 subsection {* Primitive logic *}
    38 
    38 
    39 subsubsection {* Core syntax *}
    39 subsubsection {* Core syntax *}