src/Pure/ML-Systems/smlnj-ptreql.ML
author wenzelm
Thu, 13 Apr 2006 12:01:08 +0200
changeset 19430 177e35232d1b
parent 16528 25a7459d4d4a
permissions -rw-r--r--
ProofDisplay.print_theorems/theory;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16528
25a7459d4d4a pointer equality for sml/nj
paulson
parents:
diff changeset
     1
(*  Title:      $Id$
25a7459d4d4a pointer equality for sml/nj
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson
25a7459d4d4a pointer equality for sml/nj
paulson
parents:
diff changeset
     3
25a7459d4d4a pointer equality for sml/nj
paulson
parents:
diff changeset
     4
Pointer Equality: for Standard ML of New Jersey 110.49 or later.
25a7459d4d4a pointer equality for sml/nj
paulson
parents:
diff changeset
     5
25a7459d4d4a pointer equality for sml/nj
paulson
parents:
diff changeset
     6
Thanks to Matthias Blume for providing InlineT.ptreql!
25a7459d4d4a pointer equality for sml/nj
paulson
parents:
diff changeset
     7
*)
25a7459d4d4a pointer equality for sml/nj
paulson
parents:
diff changeset
     8
25a7459d4d4a pointer equality for sml/nj
paulson
parents:
diff changeset
     9
CM.autoload "$smlnj/init/init.cmi";
25a7459d4d4a pointer equality for sml/nj
paulson
parents:
diff changeset
    10
val pointer_eq = InlineT.ptreql;