# HG changeset patch
# User sultana
# Date 1392825422 0
# Node ID 14e8e51c7fa858a3c52618dcf0dbcf91d6a49a0c
# Parent  8e6b2ad9cfe08619202df97503b6e87423471b55
edges are now being shown in the proof graph;
removed the shapes related to the conjecture and the negated conjecture, to remove clutter (since i'm also showing the inference's conclusion in latex);

diff -r 8e6b2ad9cfe0 -r 14e8e51c7fa8 src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Wed Feb 19 15:57:02 2014 +0000
@@ -40,9 +40,13 @@
   | Role_Assumption => "trapezium" (*NOTE this is not standard wrt IDV*)
   | Role_Lemma => "hexagon"
   | Role_Theorem => "star" (*NOTE this is not standard wrt IDV*)
-  | Role_Conjecture => "house"
-  | Role_Negated_Conjecture => "invhouse"
+
+  (*NOTE changed the next three to plaintext to avoid clutter, since
+         i'm also displaying the inference's conclusion in latex*)
+  | Role_Conjecture => "plaintext" (* "house" *)
+  | Role_Negated_Conjecture => "plaintext" (* "invhouse" *)
   | Role_Plain => "plaintext" (* "circle" *) (*could also use none*)
+
   | Role_Fi_Domain => raise NO_ROLE_SHAPE
   | Role_Fi_Functors => raise NO_ROLE_SHAPE
   | Role_Fi_Predicates => raise NO_ROLE_SHAPE
@@ -107,8 +111,7 @@
       "node[width=0.5];\n" ^
       "node[shape=plaintext];\n" ^
       (* "node[fillcolor=lightgray];\n" ^ *)
-      "node[fontsize=50];\n" ^
-      "edge[dir=none];\n"
+      "node[fontsize=50];\n"
   in
     TPTP_Parser.parse_file input_file
     |> map (tptp_dot_node true true)