aboutsummaryrefslogtreecommitdiffhomepage
path: root/hol-light/TacticRecording/examples3_LEMMA1.dot
diff options
context:
space:
mode:
authorGravatar mark <>2012-02-23 11:00:45 +0000
committerGravatar mark <>2012-02-23 11:00:45 +0000
commit448583e76767da575c9d90f54266d434c86282ed (patch)
treef62d7cbd6b00c9d894929d37ff261efbd7b11916 /hol-light/TacticRecording/examples3_LEMMA1.dot
parent6ecd3be998c4d2a6d8dae8ec2f67c50305a251ef (diff)
Capability for exporting .dot files added.
Diffstat (limited to 'hol-light/TacticRecording/examples3_LEMMA1.dot')
-rw-r--r--hol-light/TacticRecording/examples3_LEMMA1.dot24
1 files changed, 24 insertions, 0 deletions
diff --git a/hol-light/TacticRecording/examples3_LEMMA1.dot b/hol-light/TacticRecording/examples3_LEMMA1.dot
new file mode 100644
index 00000000..69bc7c4a
--- /dev/null
+++ b/hol-light/TacticRecording/examples3_LEMMA1.dot
@@ -0,0 +1,24 @@
+digraph G {
+ subgraph cluster0 {
+ label = "induction";
+ 517->518;
+ 517->519;
+ }
+ subgraph cluster1 {
+ label = "base case";
+ 528->528
+ }
+ subgraph cluster2 {
+ label = "step case";
+ 537->538;
+ 538->540;
+ 540->542;
+ 542->544;
+ 544->546;
+ 546->548;
+ }
+ 512->513;
+ 513->517;
+ 518->528;
+ 519->537;
+} \ No newline at end of file