# HG changeset patch # User wenzelm # Date 770478145 -7200 # Node ID c8171ee32744bdce6514047bbfdbc168827c2ae2 # Parent 54fcef4db0dba2901bc35655aff396065ecb6b4b replaced infix also by |> diff -r 54fcef4db0db -r c8171ee32744 src/Pure/library.ML --- a/src/Pure/library.ML Wed Jun 01 13:18:35 1994 +0200 +++ b/src/Pure/library.ML Wed Jun 01 15:42:25 1994 +0200 @@ -18,8 +18,8 @@ fun K x y = x; (*reverse apply*) -infix also; -fun (x also f) = f x; +infix |>; +fun (x |> f) = f x; (*combine two functions forming the union of their domains*) infix orelf; diff -r 54fcef4db0db -r c8171ee32744 src/Pure/sign.ML --- a/src/Pure/sign.ML Wed Jun 01 13:18:35 1994 +0200 +++ b/src/Pure/sign.ML Wed Jun 01 15:42:25 1994 +0200 @@ -547,27 +547,27 @@ val pure = make_sign (Syntax.type_syn, tsig0, Symtab.null) [] "#" - also add_types + |> add_types (("fun", 2, NoSyn) :: ("prop", 0, NoSyn) :: ("itself", 1, NoSyn) :: Syntax.Mixfix.pure_types) - also add_classes [([], logicC, [])] - also add_defsort logicS - also add_arities + |> add_classes [([], logicC, [])] + |> add_defsort logicS + |> add_arities [("fun", [logicS, logicS], logicS), ("prop", [], logicS), ("itself", [logicS], logicS)] - also add_syntax Syntax.Mixfix.pure_syntax - also add_trfuns Syntax.pure_trfuns - also add_consts + |> add_syntax Syntax.Mixfix.pure_syntax + |> add_trfuns Syntax.pure_trfuns + |> add_consts [("==", "['a::{}, 'a] => prop", Mixfix ("(_ ==/ _)", [3, 2], 2)), ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)), ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)), ("all", "('a => prop) => prop", Binder ("!!", 0)), ("TYPE", "'a itself", NoSyn), (Syntax.constrainC, "'a::{} => 'a", NoSyn)] - also add_name "Pure"; + |> add_name "Pure"; end;