# HG changeset patch
# User wenzelm
# Date 1135958218 -3600
# Node ID 57b489b54914a1d06eaa33b684197223cbf1fd4f
# Parent  9446cb8e1f655fa7b791cdac54fce1b249377fd9
provide equality_name, not_name;

diff -r 9446cb8e1f65 -r 57b489b54914 src/FOL/blastdata.ML
--- a/src/FOL/blastdata.ML	Fri Dec 30 16:56:57 2005 +0100
+++ b/src/FOL/blastdata.ML	Fri Dec 30 16:56:58 2005 +0100
@@ -3,6 +3,8 @@
 structure Blast_Data = 
   struct
   type claset	= Cla.claset
+  val equality_name = "op ="
+  val not_name = "Not"
   val notE	= notE
   val ccontr	= ccontr
   val contr_tac = Cla.contr_tac
diff -r 9446cb8e1f65 -r 57b489b54914 src/HOL/blastdata.ML
--- a/src/HOL/blastdata.ML	Fri Dec 30 16:56:57 2005 +0100
+++ b/src/HOL/blastdata.ML	Fri Dec 30 16:56:58 2005 +0100
@@ -16,6 +16,8 @@
 structure Blast_Data = 
   struct
   type claset	= Classical.claset
+  val equality_name = "op ="
+  val not_name = "Not"
   val notE	= notE
   val ccontr	= ccontr
   val contr_tac = Classical.contr_tac