src/FOL/FOL.thy
changeset 42453 cd5005020f4e
parent 41827 98eda7ffde79
child 42455 6702c984bf5a
     1.1 --- a/src/FOL/FOL.thy	Fri Apr 22 00:57:59 2011 +0200
     1.2 +++ b/src/FOL/FOL.thy	Fri Apr 22 12:46:48 2011 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4  
     1.5  (*** Tactics for implication and contradiction ***)
     1.6  
     1.7 -(*Classical <-> elimination.  Proof substitutes P=Q in 
     1.8 +(*Classical <-> elimination.  Proof substitutes P=Q in
     1.9      ~P ==> ~Q    and    P ==> Q  *)
    1.10  lemma iffCE:
    1.11    assumes major: "P<->Q"
    1.12 @@ -305,7 +305,19 @@
    1.13  
    1.14  
    1.15  use "simpdata.ML"
    1.16 -setup simpsetup
    1.17 +ML {*
    1.18 +(*intuitionistic simprules only*)
    1.19 +val IFOL_ss =
    1.20 +  FOL_basic_ss
    1.21 +  addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps})
    1.22 +  addsimprocs [defALL_regroup, defEX_regroup]
    1.23 +  addcongs [@{thm imp_cong}];
    1.24 +
    1.25 +(*classical simprules too*)
    1.26 +val FOL_ss = IFOL_ss addsimps (@{thms cla_simps} @ @{thms cla_ex_simps} @ @{thms cla_all_simps});
    1.27 +*}
    1.28 +
    1.29 +setup {* Simplifier.map_simpset (K FOL_ss) *}
    1.30  setup "Simplifier.method_setup Splitter.split_modifiers"
    1.31  setup Splitter.setup
    1.32  setup clasimp_setup