| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | available.txt | 2 | logplain |
| -rw-r--r-- | expt.csv | 511 | logplain |
| -rw-r--r-- | expt_names | 133 | logplain |
| -rw-r--r-- | expt_tactics.csv | 542 | logplain |
| -rw-r--r-- | factorial.csv | 497 | logplain |
| -rw-r--r-- | factorial_names | 133 | logplain |
| -rw-r--r-- | factorial_tactics.csv | 545 | logplain |
| -rw-r--r-- | fib.csv | 560 | logplain |
| -rw-r--r-- | fib_names | 127 | logplain |
| -rw-r--r-- | fib_tactics.csv | 584 | logplain |
| -rw-r--r-- | lessp.csv | 461 | logplain |
| -rw-r--r-- | lessp_names | 133 | logplain |
| -rw-r--r-- | lessp_tactics.csv | 538 | logplain |
| -rw-r--r-- | m1.csv | 214 | logplain |
| -rw-r--r-- | m1_names | 37 | logplain |
| -rw-r--r-- | m1_tactics.csv | 208 | logplain |
| -rw-r--r-- | multiplication.csv | 487 | logplain |
| -rw-r--r-- | multiplication_names | 127 | logplain |
| -rw-r--r-- | multiplication_tactics.csv | 542 | logplain |
| -rw-r--r-- | power.csv | 507 | logplain |
| -rw-r--r-- | power_names | 139 | logplain |
| -rw-r--r-- | power_tactics.csv | 540 | logplain |
 |
index : proof-general | |
| Emacs interface for proof assistants |
| aboutsummaryrefslogtreecommitdiffhomepage |