src/FOL/simpdata.ML
changeset 32177 bc02c5bfcb5b
parent 32155 e2bf2f73b0c8
child 32952 aeb1e44fbc19
     1.1 --- a/src/FOL/simpdata.ML	Fri Jul 24 21:21:45 2009 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Fri Jul 24 21:34:37 2009 +0200
     1.3 @@ -95,27 +95,25 @@
     1.4  
     1.5  (*** Case splitting ***)
     1.6  
     1.7 -structure SplitterData =
     1.8 -  struct
     1.9 -  structure Simplifier = Simplifier
    1.10 -  val mk_eq          = mk_eq
    1.11 +structure Splitter = Splitter
    1.12 +(
    1.13 +  val thy = @{theory}
    1.14 +  val mk_eq = mk_eq
    1.15    val meta_eq_to_iff = @{thm meta_eq_to_iff}
    1.16 -  val iffD           = @{thm iffD2}
    1.17 -  val disjE          = @{thm disjE}
    1.18 -  val conjE          = @{thm conjE}
    1.19 -  val exE            = @{thm exE}
    1.20 -  val contrapos      = @{thm contrapos}
    1.21 -  val contrapos2     = @{thm contrapos2}
    1.22 -  val notnotD        = @{thm notnotD}
    1.23 -  end;
    1.24 +  val iffD = @{thm iffD2}
    1.25 +  val disjE = @{thm disjE}
    1.26 +  val conjE = @{thm conjE}
    1.27 +  val exE = @{thm exE}
    1.28 +  val contrapos = @{thm contrapos}
    1.29 +  val contrapos2 = @{thm contrapos2}
    1.30 +  val notnotD = @{thm notnotD}
    1.31 +);
    1.32  
    1.33 -structure Splitter = SplitterFun(SplitterData);
    1.34 -
    1.35 -val split_tac        = Splitter.split_tac;
    1.36 +val split_tac = Splitter.split_tac;
    1.37  val split_inside_tac = Splitter.split_inside_tac;
    1.38 -val split_asm_tac    = Splitter.split_asm_tac;
    1.39 -val op addsplits     = Splitter.addsplits;
    1.40 -val op delsplits     = Splitter.delsplits;
    1.41 +val split_asm_tac = Splitter.split_asm_tac;
    1.42 +val op addsplits = Splitter.addsplits;
    1.43 +val op delsplits = Splitter.delsplits;
    1.44  
    1.45  
    1.46  (*** Standard simpsets ***)