liamoc.net
my forest
isa: todo list added
+39
-2
+1
-1
trees/index.tree
+1
-1
trees/index.tree
+1
-1
trees/isa/isa-0001.tree
+1
-1
trees/isa/isa-0001.tree
+37
trees/isa/isa-001B.tree
+37
trees/isa/isa-001B.tree
···
32
32
\transclude{isa-001J}
33
33
\transclude{isa-001L}
34
34
\transclude{isa-001M}
35
+
\ul{
36
+
\li{natural numbers}
37
+
\li{Fun command}
38
+
\li{rpt}
39
+
\li{induct method (structural)}
40
+
\li{rpt twice theorem}
41
+
\li{twos type}
42
+
\li{prepend}
43
+
\li{prepend prepend theorem}
44
+
\li{semicolon operator}
45
+
\li{append}
46
+
\li{append prepend theorem}
47
+
\li{append assoc}
48
+
\li{lists (replicate function)}
49
+
\li{decompress}
50
+
\li{compress}
51
+
\li{decompress compress thm}
52
+
\li{compress app}
53
+
\li{compress replicate}
54
+
\li{inductive predicates}
55
+
\li{rule induction}
56
+
\li{wellformedness}
57
+
\li{compress decompress thm}
58
+
\li{arbitrary}
59
+
\li{chaining}
60
+
\li{repeating}
61
+
\li{subsequence example}
62
+
\li{subsequence theorems}
63
+
\li{safe vs unsafe rules}
64
+
\li{intro, elim, clarify, blast, (fast,slow,best)}}
65
+
\li{automation: clarsimp, auto, fastforce (slowsimp, bestsimp), force}
66
+
\li{sledgehammer, try, find_theorems}
67
+
\li{clarify, clarsimp}
68
+
\li{structured proofs}
69
+
\li{calculational proofs}
70
+
\li{examples examples examples}
71
+
}