Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
provide equality_name, not_name;
authorwenzelm
Fri, 30 Dec 2005 16:56:58 +0100
changeset 18524 57b489b54914
parent 18523 9446cb8e1f65
child 18525 ce1ae48c320f
provide equality_name, not_name;
src/FOL/blastdata.ML file | annotate | diff | comparison | revisions
src/HOL/blastdata.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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
isabelle