adapted ZF,FOL,CCL,LCF to modified splitter
authornipkow
Tue, 09 Aug 2016 18:09:32 +0200
changeset 63637 9a57baa15e1b
parent 63636 6f38b7abb648
child 63638 5c6da7213e9b
adapted ZF,FOL,CCL,LCF to modified splitter
src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Tue Aug 09 17:00:36 2016 +0200
+++ b/src/FOL/simpdata.ML	Tue Aug 09 18:09:32 2016 +0200
@@ -97,6 +97,7 @@
   val contrapos = @{thm contrapos}
   val contrapos2 = @{thm contrapos2}
   val notnotD = @{thm notnotD}
+  val safe_tac = Cla.safe_tac
 );
 
 val split_tac = Splitter.split_tac;