| changeset 18524 | 57b489b54914 |
| parent 18171 | c4f873d65603 |
| child 20944 | 34b2c1bb7178 |
--- 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