How to turn lecture slides into study-ready notes on Mac

Lecture slides are designed to present a topic, not to become your personal notes. The important definitions, examples, diagrams, and formulas may be spread across a PDF, course portal, recording, or presentation.

Snapdown lets you capture only the useful sections and combine them into one Markdown document. You can paste that document into Obsidian or another notes app, add your own explanation, and use it for revision without rebuilding every slide by hand.

For this example, I captured six pages from the Tamarin Prover Tutorial slides. They include headings, nested lists, equations, transition rules, and worked traces.

Capture several slides as one note

1. Select Markdown output in Snapdown.
2. If Aggregate Mode is off, press Command+Shift+A to turn it on.
3. Press Command+Shift+2 and select the important part of the first slide.
4. Repeat for the remaining slides in the order you want them to appear.
5. Focus your destination note and press Command+Shift+V to paste the complete document and start a new one.

Aggregate Mode appends each successful capture to the current Markdown document. A horizontal separator can keep the slide regions distinct while you review the result.

Capture only the material you need. A tight region gives the recognizer less navigation, browser chrome, or presentation UI to interpret. Keep a diagram inside the crop when it matters, then add a short explanation of its spatial meaning to your notes.

The final Markdown output

Here is the complete unedited output from Snapdown 1.1.0. The headings, lists, examples, and traces came through well. The main cleanup was concentrated in a few notation-heavy expressions, which I cover below.

# Tamarin: high-level

- **Modeling** protocol & adversary done using multiset rewriting
  - Specifies transition system; induces set of traces

- **Property** specification using fragment of first-order logic
  - Specifies “good” traces

- Tamarin tries to
  - provide proof that all system traces are good, or
  - construct a counterexample trace of the system (attack)

# Modeling in Tamarin

- **Multiset rewriting**; surprisingly similar to “oracles”
- **Basic ingredients**:
  - **Terms** (think “messages”)
  - **Facts** (think “sticky notes on the fridge”)
  - Special facts: $\text{Fr}(t)$ , $\text{In}(t)$ , $\text{Out}(t)$ , $\text{K}(t)$
- **State of system is a multiset of facts**
  - **Initial state** is the empty multiset
  - **Rules** specify the transition rules (“moves”)
- **Rules are of the form**:
  - $l \rightarrow r$
  - $l \rightarrow [a] \rightarrow r$

# The model

- **Term algebra**
  - $enc(\_,\_), dec(\_,\_), h(\_,\_), \_^ \_, \_^{-1}, \_ * \_, 1, \ldots$

- **Equational theory**
  - $dec(enc(m,k),k) =_E m,$
  - $(x^{\wedge}y)^{\wedge}z =_E x^{\wedge}(y^*z),$
  - $(x^{-1})^{-1} =_E x, \ldots$

- **Facts**
  - $F(t1,\ldots,tn)$

- **Transition system**
  - State: multiset of facts
  - Rules: $ l \rightarrow [ a ] \rightarrow r $

- **Tamarin-specific**
  - Built-in Dolev-Yao attacker rules
    - $ \text{In}( ) $ , $ \text{Out}( ) $ , $ \text{K}( ) $
  - Special **Fresh** rule:
    - $ [] \rightarrow [] \rightarrow [ \text{Fr}(x) ] $
      - With additional constraints on systems such that $ x $ unique

# Semantics

- **Transition relation**

  $S \multimap [a] \rightarrow_R ((S \not\# I) \cup\# r)$

  where $I \multimap [a] \rightarrow r$ is a ground instance of a rule and $I \subseteq\# S$

- **Executions**

  $\text{Exec}(R) = \{ [\,] \multimap [a_1] \rightarrow \ldots \multimap [a_n] \rightarrow S_n \mid \forall n \, . \, \text{Fr}(n) \text{ appears only once on rhs} \}$

- **Traces**

  $\text{Traces}(R) = \{ [a_1, \ldots, a_n] \mid [\,] \multimap [a_1] \rightarrow \ldots \multimap [a_n] \rightarrow S_n \in \text{Exec}(R) \}$

# Semantics: example 1

## Rules

- rule 1: [ ] —[ Init() ]→ [ A('5') ]
- rule 2: [ A(x) ] —[ Step(x) ]→ [ B(x) ]

## Execution example

- [ ]
- —[ Init() ]→ [ A('5') ]
- —[ Init() ]→ [ A('5'), A('5') ]
- —[ Step('5') ]→ [ A('5'), B('5') ]

## Corresponding trace

- [ Init(), Init(), Step('5') ]

# Semantics: example 2 (persistent facts)

## Rules

- rule1: [ ] —[ Init() ]→ [ !C('ok'), D('1') ]
- rule2: [ !C(x), D(y) ] —[ Step(x,y) ]→ [ D(h(y)) ]

## Execution example

- [ ]
- —[ Init() ]→ [ !C('ok'), D('1' ) ]
- —[ Step('ok','1' ) ]→ [ !C('ok'), D(h('1') ) ]
- —[ Step('ok',h('1') ) ]→ [ !C('ok'), D(h(h('1')) ) ]

## Corresponding trace

- [ Init(), Step('ok', '1'), Step('ok', h('1')) ]

What came through well

Snapdown kept all six captures and headings in order. It also preserved all four special facts, five model categories, four concrete example rules, eight execution entries, and both corresponding traces. No structural reconstruction was needed.

The prose needed one small addition: the slides' legend explaining that quoted values are constants. Eight formal expressions needed notation cleanup, mostly because one labeled transition arrow was represented as two arrows. The ordinary headings, lists, explanations, and worked examples were otherwise ready to use.

For formula-heavy material, make one quick pass over the notation you plan to study. Check arrows, brackets, subscripts, and operators against the slide. For ordinary prose and lists, a brief scan is usually enough.

Turn your notes into active practice

Once the note looks right, it can become context for a study agent. Instead of asking for another summary, ask it to test your recall or create a small worked problem.

Generate active-recall questions

Act as my study coach. Use only the lecture note below.

Ask one active-recall question at a time. Do not reveal the answer until I
respond. Mark my answer correct, partially correct, or incorrect, explain the
judgment from the note, then ask a short follow-up about what I missed.

If the note does not contain enough information, say so instead of adding
outside facts.

[PASTE THE NOTE HERE]

Practice with worked traces

Use only the lecture note below to create one small Tamarin-style rewriting
problem. Ask me which rule can fire, which facts are consumed and produced, and
which action is added to the trace.

Do not provide the solution until I answer. Then identify my first incorrect
step and create a slightly harder variant by changing one fact or rule.

[PASTE THE NOTE HERE]

Snapdown processes the slide captures locally on Apple silicon. If you paste the note into a cloud-hosted AI service, that separate service receives the text, so keep private or restricted course material out of the prompt.

The useful boundary

Snapdown handles the repetitive part: collecting selected screen regions and turning them into one structured document. You still choose what matters, make a quick check where notation is important, and add the explanations that help the material make sense to you.

Try the first 10 successful captures free. Snapdown is a $12 USD one-time purchase for Apple silicon Macs running macOS 14 or later.

Source note

The selected material comes from the Tamarin Prover Tutorial morning slides by David Basin, Cas Cremers, Jannik Dreier, and Ralf Sasse. The teaching-material repository licenses all its materials under Creative Commons Attribution 4.0 International. That licence permits sharing and adaptation, including commercial use, with attribution and disclosure of changes. Six slide regions were captured and combined into Markdown; no endorsement is implied.