src/FOL/FOL.thy
changeset 11771 b7b100a2de1d
parent 11678 6aa3e2d26683
child 11848 6e3017adb8c0
equal deleted inserted replaced
11770:b6bb7a853dd2 11771:b7b100a2de1d
    33 use "simpdata.ML"
    33 use "simpdata.ML"
    34 setup simpsetup
    34 setup simpsetup
    35 setup "Simplifier.method_setup Splitter.split_modifiers"
    35 setup "Simplifier.method_setup Splitter.split_modifiers"
    36 setup Splitter.setup
    36 setup Splitter.setup
    37 setup Clasimp.setup
    37 setup Clasimp.setup
    38 setup Rulify.setup
       
    39 
       
    40 
    38 
    41 
    39 
    42 subsection {* Proof by cases and induction *}
    40 subsection {* Proof by cases and induction *}
    43 
    41 
    44 text {* Proper handling of non-atomic rule statements. *}
    42 text {* Proper handling of non-atomic rule statements. *}