# HG changeset patch
# User wenzelm
# Date 1005511084 -3600
# Node ID 7cf8574102d5e1c2c76f3071d9930c58fe5420bf
# Parent  a57873aec3bff495b3ec6fa9a60ddb925beb7209
pure_syntax_output: "_meta_conjunction";

diff -r a57873aec3bf -r 7cf8574102d5 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Sun Nov 11 21:37:44 2001 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Sun Nov 11 21:38:04 2001 +0100
@@ -31,6 +31,7 @@
   val mixfix_args: mixfix -> int
   val pure_nonterms: string list
   val pure_syntax: (string * string * mixfix) list
+  val pure_syntax_output: (string * string * mixfix) list
   val pure_appl_syntax: (string * string * mixfix) list
   val pure_applC_syntax: (string * string * mixfix) list
   val pure_xsym_syntax: (string * string * mixfix) list
@@ -240,6 +241,10 @@
   ("_noindex",     "index",                         Delimfix ""),
   ("_struct",      "index => logic",                Delimfix "\\<struct>_")];
 
+val pure_syntax_output =
+ [("Goal", "prop => prop", Mixfix ("_", [0], 0)),
+  ("_meta_conjunction", "prop => prop => prop", InfixrName ("&&", 2))];
+
 val pure_appl_syntax =
  [("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri)),
   ("_appl", "[('b => 'a), args] => aprop", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri))];