# HG changeset patch # User wenzelm # Date 857743500 -3600 # Node ID b3a03fc4deee5a3b5cd4636fbee3311278e655d1 # Parent 2ade3a1419344cdda1054a86a549e9af019dcd76 removed (| |) symbols syntax; diff -r 2ade3a141934 -r b3a03fc4deee src/HOLCF/Sprod3.thy --- a/src/HOLCF/Sprod3.thy Fri Mar 07 15:03:57 1997 +0100 +++ b/src/HOLCF/Sprod3.thy Fri Mar 07 15:05:00 1997 +0100 @@ -23,9 +23,6 @@ "(|x, y, z|)" == "(|x, (|y, z|)|)" "(|x, y|)" == "spair`x`y" -syntax (symbols) - "@stuple" :: "['a, args] => 'a ** 'b" ("(1\\_,/ _\\)") - defs spair_def "spair == (LAM x y.Ispair x y)" sfst_def "sfst == (LAM p.Isfst p)"