src/FOL/FOL.thy
changeset 9885 34494703d283
parent 9713 2c5b42311eb0
child 10130 5a2e00bf1e42
equal deleted inserted replaced
9884:8cc344b3435e 9885:34494703d283
    56 use "simpdata.ML"
    56 use "simpdata.ML"
    57 setup simpsetup
    57 setup simpsetup
    58 setup "Simplifier.method_setup Splitter.split_modifiers"
    58 setup "Simplifier.method_setup Splitter.split_modifiers"
    59 setup Splitter.setup
    59 setup Splitter.setup
    60 setup Clasimp.setup
    60 setup Clasimp.setup
       
    61 setup Rulify.setup
    61 
    62 
    62 
    63 
    63 subsection {* Calculational rules *}
    64 subsection {* Calculational rules *}
    64 
    65 
    65 lemma forw_subst: "a = b ==> P(b) ==> P(a)"
    66 lemma forw_subst: "a = b ==> P(b) ==> P(a)"