Remove option aspect of 'finfo' datatype, and rename datatype to 'mldata'.

Add wrapper function for :thm -> thm list.
Promote more objects.

1 files changed, 20 insertions, 9 deletions

diff --git a/hol-light/TacticRecording/ex.dot b/hol-light/TacticRecording/ex.dot
index fbe961bd..e96142f9 100644
--- a/hol-light/TacticRecording/ex.dot
+++ b/hol-light/TacticRecording/ex.dot
@@ -1,13 +1,24 @@
 digraph G {
-  subgraph cluster0 {
-    label = "process #1"
-    a0->a1->a2->a3
-  }
   subgraph cluster1 {
-    label = "process #2"
-    b0->b1->b2->b3
+    label = "induction";
+    517 -> 518;
+    517 -> 519;
+  }
+  subgraph cluster2 {
+    label = "base case";
+    528;
+  }
+  subgraph cluster3 {
+    label = "step case";
+    537 -> 538;
+    538 -> 540;
+    540 -> 542;
+    542 -> 544;
+    544 -> 546;
+    546 -> 548;
   }
-  b3->23
-  b2->a3
-  a3->23
+  512 -> 513;
+  513 -> 517;
+  518 -> 528;
+  519 -> 537;
 }
\ No newline at end of file