src/FOL/simpdata.ML
changeset 5307 6a699d5cdef4
parent 5304 c133f16febc7
child 5496 42d13691be86
equal deleted inserted replaced
5306:3d1368a3a2a2 5307:6a699d5cdef4
   257 structure Splitter = SplitterFun(SplitterData);
   257 structure Splitter = SplitterFun(SplitterData);
   258 
   258 
   259 val split_tac        = Splitter.split_tac;
   259 val split_tac        = Splitter.split_tac;
   260 val split_inside_tac = Splitter.split_inside_tac;
   260 val split_inside_tac = Splitter.split_inside_tac;
   261 val split_asm_tac    = Splitter.split_asm_tac;
   261 val split_asm_tac    = Splitter.split_asm_tac;
   262 val addsplits        = Splitter.addsplits;
   262 val op addsplits     = Splitter.addsplits;
   263 val delsplits        = Splitter.delsplits;
   263 val op delsplits     = Splitter.delsplits;
   264 val Addsplits        = Splitter.Addsplits;
   264 val Addsplits        = Splitter.Addsplits;
   265 val Delsplits        = Splitter.Delsplits;
   265 val Delsplits        = Splitter.Delsplits;
   266 
   266 
   267 
   267 
   268 (*** Standard simpsets ***)
   268 (*** Standard simpsets ***)