diff options
author | mark <> | 2012-02-23 17:12:05 +0000 |
---|---|---|
committer | mark <> | 2012-02-23 17:12:05 +0000 |
commit | 4ed83bcb88f220cc08c3223bd4f274eaa5f31e0c (patch) | |
tree | 7bbf95ed0b561cfdf2e491ca8b6d614b9cdf0e49 /hol-light/TacticRecording/ex3b.dot | |
parent | f1fdbc36e57c6005aed913830eabe2115dabc7c5 (diff) |
Altered graph .dot export so that nodes are displayed as their tactic.
Diffstat (limited to 'hol-light/TacticRecording/ex3b.dot')
-rw-r--r-- | hol-light/TacticRecording/ex3b.dot | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/hol-light/TacticRecording/ex3b.dot b/hol-light/TacticRecording/ex3b.dot new file mode 100644 index 00000000..5b951b96 --- /dev/null +++ b/hol-light/TacticRecording/ex3b.dot @@ -0,0 +1,37 @@ +digraph G { + 344 [label = "CONV_TAC"]; + 345 [label = "GEN_TAC"]; + 351 [label = "INDUCT_TAC"]; + 352 [label = "REWRITE_TAC"]; + 358 [label = "REAL_ARITH_TAC"]; + 353 [label = "REWRITE_TAC"]; + 367 [label = "REWRITE_TAC"]; + 368 [label = "SIMP_TAC"]; + 370 [label = "REWRITE_TAC"]; + 372 [label = "REWRITE_TAC"]; + 374 [label = "ASM_REWRITE_TAC"]; + 376 [label = "REWRITE_TAC"]; + 378 [label = "REAL_ARITH_TAC"]; + 344 -> 345; + 345 -> 351; + subgraph cluster1 { + label = "induction"; + 351 -> 352; + 351 -> 353; + 352 -> 358; + subgraph cluster2 { + label = "base case"; + 358; + } + 353 -> 367; + subgraph cluster3 { + label = "step case"; + 367 -> 368; + 368 -> 370; + 370 -> 372; + 372 -> 374; + 374 -> 376; + 376 -> 378; + } + } +}
\ No newline at end of file |