diff --git a/assets/isabelle_hol.svg b/assets/isabelle_hol.svg
new file mode 100644
index 0000000..27125db
--- /dev/null
+++ b/assets/isabelle_hol.svg
@@ -0,0 +1,363 @@
+
+
diff --git a/assets/music.tsv b/assets/music.tsv
index 99b9e13..0273ad7 100644
--- a/assets/music.tsv
+++ b/assets/music.tsv
@@ -1,600 +1,605 @@
-Composer Title Where
-Aichinger Factus est repente 4thCh p2
-Aichinger Regina caeli 4thCh p7
-Amner Lift up your heads O ye gates XVIAB p41
-Amner O God my King AfC1 p130
-Anerio Alleluia. Christus surrexit Ash p156
-Anerio Christus factus est Ash p52; 1stCh p1
-Anerio, G. F. Requiem aeternam 1stCh p4
-Anon. Easter Alleluias: (a) Antiphon with psalm tone, (b) Plainchant Alleluia Ash p154
-Anon. Come, rock the cradle for him CfC3 p53
-Anon. (16th Century) O Lord, the maker of all thing XVIAB p85
-Anon. (16th Century) Rejoice in the Lord alway XVIAB p1; Adv p162
-Anon. (16th Century) This is the day XVIAB p32
-Arcadelt Haec dies NCAB p146; 5thCh p2
-Arcadelt O Lord, my God, to thee NCAB p293
-Arcadelt (attrib.) Ave Maria NOEAB p12
-Archer Advent Wreath Prayers Adv p16
-Archer And I saw a new heaven NOEAB p6
-Archer Ave Maria Adv p33
-Archer Creator of the stars of night Adv p56
-Archer Prayer for the Blessing of Light Adv p160
-Archer The Linden Tree Carol Adv p180
-Archer The Lord goes up NOEAB p210
-Archer (arr.) Alma redemptoris mater Adv p22
-Archer (arr.) On Jordan's bank Adv p146
-Archer (arr.) People, look East NOEAB p176
-Archer (arr.) The Angel Gabriel Adv p171
-Armstrong Gibbs Bless the Lord, O my soul OEAB p91
-Armstrong Gibbs O, praise God in His holiness OEAB p112
-Armstrong Gibbs The strife is o'er OEAB p46
-Armstrong Gibbs While the shepherds were watching CfC1 p168
-Arne Help me, O Lord OEAB p133
-Aston I give you a new commandment NOEAB p93
-Aston So they gave their bodies NCAB p416
-Attwood Come, Holy Ghost NCAB p100; NOEAB p40
-Attwood O God, who by the leading of a star AfC1 p123
-Attwood Teach me, O Lord NOEAB p206; AfC1 p196
-Attwood Turn thy face from my sins NCAB p494
-Bach, J.S. All people at this hour OEAB p78
-Bach, J.S. Awake us, Lord, and hasten AfC1 p34
-Bach, J.S. Awake, thou wintry earth NCAB p53
-Bach, J.S. Come sweetest death OEAB p134
-Bach, J.S. Dearest Lord Jesu OEAB p1
-Bach, J.S. Flocks in pastures green abiding OEAB p136
-Bach, J.S. Forget me not OEAB p141
-Bach, J.S. God is living, God is here AfC1 p212
-Bach, J.S. God is our hope and strength AfC1 p59
-Bach, J.S. Here lies He now OEAB p25
-Bach, J.S. Jesu, hope of men despairing OEAB p35
-Bach, J.S. Jesu, joy of man's desiring NCAB p185; NOEAB p101
-Bach, J.S. Jesu, lead my footsteps ever NCAB p193
-Bach, J.S. King of glory, King of peace NCAB p201
-Bach, J.S. St. Matthew Passion Loose, Novello edition
-Bach, J.S. Subdue us by Thy goodness NCAB p421
-Bach, J.S. Up, up, my heart! with gladness AfC1 p206
-Bach, J.S. Wie soll ich dich empfangen (from The Christmas Oratorio) Adv p213
-Bach, J.S. Ah! dearest Jesu (from The Christmas Oratorio) CfC3 p22
-Bach, J.S. And there were shepherds CfC1 p10
-Bach, J.S. With all thy hosts (from The Christmas Oratorio) CfC3 p22
-Bach, J.S. Zion hört die Wächter singen CfC2 p214
-Bach, J.S. (harm.) O little one sweet CfC1 p87
-Bain Brother James' Air NOEAB p30
-Bainton A babe is born I wys CfC2 p6
-Bairstow I sat down under his shadow AfC1 p74
-Bairstow Jesu, the very thought of thee NCAB p197
-Bairstow Let all mortal flesh keep silence AfC4 p88
-Bairstow Psalm 114 Ash p165
-Bairstow The day draws on with golden light NCAB p436
-Bairstow The Lamentation Ash p55
-Bairstow Though I speak with the tongues of men NCAB p484
-Bairstow (after Gibbons) Jesu, grant me this I pray Ash p60
-Ballet Lute-book lullaby CfC1 p108
-Barcrofte O almighty God AfC1 p112
-Barnard (arr.) In the heart where love is abiding Ash p100
-Batten Deliver us, O Lord our God XVIAB p99
-Batten Haste thee, O God AfC1 p64
-Batten Let my complaint come before thee XVIAB p24
-Batten Lord, we beseech thee XVIAB p20
-Batten O praise the Lord OBTA p251
-Batten O sing joyfully XVIAB p70
-Batten When the Lord turned again XVIAB p35
-Bax Lord, thou hast told us AfC4 p28
-Bennett Out of your sleep CfC2 p150
-Bennett Susanni CfC3 p18
-Bennett What sweeter music CfC3 p192
-Berkeley I sing of a maiden Adv p109
-Berlioz The Shepherd's farewell CfC1 p142
-Berry (arr.) Advent Antiphons (Latin) Adv p8
-Bevan There's a wideness in God's mercy NOEAB p224
-Bevan (arr.) O Thou who at Thy Eucharist did'st pray OEAB p99
-Bevan (arr) O love of whom is truth and light OEAB p144
-Blackwell (arr.) O Thou, whose all-redeeming might NOEAB p168
-Blow Let my prayer AfC1 p86
-Blow Praise the Lord, ye servants AfC1 p174
-Bohemian Brethren (arr. Guest) Zion, at thy shining gates Adv p214
-Bourgeois O gladsome light, O grace NCAB p273
-Bourgeois O strength and stay AfC1 p156
-Bourne Thou art God NOEAB p231
-Brahms Ah, thou poor world AfC1 p10
-Britten A boy was born CfC1 p4
-Britten A new year carol CfC2 p64
-Britten Corpus Christi Carrol Loose. Oxford Edition.
-Britten O be joyful in the Lord (Jubilate Deo) AfC4 p140
-Britten There is no rose CfC3 p181
-Bruckner Locus iste NCAB p222
-Bruckner Pange lingua (Of the glorious Body telling) Ash p104
-Bruckner Virga Jesse floruit Adv p204
-Bull In the departure of the Lord Ash p123
-Bullard For all thy saints NOEAB p65
-Bullard Praise ye the Lord NOEAB p180
-Bullard Star of the East NOEAB p198
-Bullard The Feast of Palms Ash p74
-Bullock Give us the wings of faith AfC4 p128
-Bullock Good Christian men rejoice and sing OEAB p38
-Bullock (arr.) Give laud unto the Lord OEAB p64
-Byrd Ave verum corpus NCAB p38; OBTA p44; 2ndCh p2
-Byrd Cibavit eos 2ndCh p6
-Byrd Civitas sancti tui Ash p4
-Byrd Haec dies OBTA p84
-Byrd Justorum animae OBTA p131
-Byrd Laetentur coeli OBTA p137
-Byrd Mass for five voices Loose. Chester edition
-Byrd Miserere mei OBTA p157
-Byrd O quam gloriosum OBTA p256
-Byrd Sacerdotes Domini NCAB p399; XVIAB p55
-Byrd Senex puerum 2ndCh p10
-Byrd Sing joyfully OBTA p287
-Byrd Teach me, O Lord OBTA p298
-Byrd This day Christ was born OBTA p307
-Byrd Venite comedite 2ndCh p13
-Campbell (arr.) Praise to God in the highest AfC1 p179
-Carter For the beauty of the earth NOEAB p70
-Carter Holy Spirit, truth divine NOEAB p84
-Carter Mary's Magnificat NCAB p231
-Carter O Lord, open thou our lips NCAB p295
-Carter (arr.) Angelus ad Virginem Adv p24
-Carter (arr.) Joy is come NOEAB p116; Ash p167
-Cashmore (after Praetorius) Es ist ein Ros' entsprungen 74Adv p
-Charpentier Salve puerule CfC3 p154
-Chilcott Be thou my vision NOEAB p23
-Chilcott God so loved the world Ash p64
-Chilcott Nova! nova! Adv p137
-Chilcott (arr.) Were you there? Ash p126
-Clarke-Whitfeld Behold, how good and joyful AfC1 p38
-Clemens non Papa Crux fidelis 5thCh p5
-Cleobury (arr.) Advent Antiphons (English) Adv p3
-Cleobury (arr.) Advent Prose (English) Adv p11
-Cleobury (arr.) Advent Prose (Latin) Adv p14
-Cleobury (arr.) Come, thou Redeemer of the earth Adv p54
-Cleobury (arr.) Let all mortal flesh keep silence Adv p115
-Cleobury (arr.) Man, assay Adv p127
-Cleobury (arr.) The Cherry Tree Carol Adv p174
-Coleman (arr.) Ye servants of God OEAB p108
-Cooke O men from the fields CfC1 p94
-Cope He is risen OEAB p42
-Cope Pleasure it is OEAB p88
-Cornelius The Three Kings CfC1 p136
-Corrêa O vos omnes NOEAB p174; AfC1 p163
-Croce O sacrum convivium 1stCh p6
-Croce O vos omnes Ash p129
-Crotch Be peace on earth OEAB p147
-Crotch Comfort, O Lord, the soul of thy servant NCAB p110
-Darke Communion Service in F Loose. Oxford Edition.
-Darlington (arr.) Jacob's Ladder Adv p110
-de Séverac Tantum ergo Ash p108
-Dering Above Him stood the Seraphim OEAB p155
-Dering Factum est silentium OBTA p57
-Dowland He that is down needs fear no fall OEAB p160
-Dowland My spirit longs for Thee OEAB p102
-Drayton Jesu dulcis memoria AfC4 p166
-Drese Round me falls the night NCAB p381
-Ebeling All my heart this night rejoices CfC2 p12
-Eccard When to the temple Mary went NCAB p516
-Elgar Ave verum corpus NCAB p44
-Elgar Dream of Gerontius Loose. 1900 Novello edition
-Elgar Light of the World Ash p170
-Elgar O salutaris Hostia No. 3 NOEAB p157
-Ellis There is no rose NOEAB p221
-Esquivel Ego sum panis vivus 3rdCh p2
-Este's Psalter While shepherds watched their flocks by night CfC1 p166 (arr. Ravenscroft), CfC2 p210 (arr. Willcocks)
-Farrant Call to remembrance NCAB p87; OBTA p50
-Farrant Hide not thou thy face NCAB p151; OBTA p94
-Farrant (attrib.) Lord, for thy tender mercy's sake NOEAB p138; NCAB p224; OBTA p152; Ash p13
-Farrar Almighty God, the fountain of all wisdom AfC1 p24
-Ferguson (arr.) People look East Adv p157
-Ford Almighty God, which hast me brought NCAB p21; AfC1 p28
-Foster Christ the Lord is risen again! NOEAB p39
-Gardiner Evening Hymn NCAB p120
-Gauntlett Once in royal David's city CfC1 p100 (arr. Mann), CfC2 p148 (arr. Mann and Willcocks)
-Gesius Hosianna dem Sohne Davids Ash p82
-Gibbons Almighty and everlasting God NCAB p18; OBTA p15
-Gibbons Drop, drop, slow tears NOEAB p52; NCAB p116
-Gibbons Hosanna to the Son of David OBTA p99
-Gibbons O clap your hands OBTA p164
-Gibbons O Lord, in thy wrath OBTA p231
-Gibbons Song 44 AfC1 p46
-Gibbons Song 46 AfC1 p30
-Gibbons This is the record of John NCAB p454; OBTA p318
-Gilbert Let all the world OEAB p119
-Goldschmidt A tender shoot Adv p31
-Goss God so loved the world NCAB p145
-Goss If we believe NCAB p168
-Goss O pray for the peace of Jerusalem AfC1 p146
-Goss O Saviour of the world NCAB p323; NOEAB p163
-Goss See amid the winter's snow CfC1 p103
-Goss These are they which follow the Lamb AfC1 p200
-Greene Thou visitest the earth NCAB p473
-Gritton Lord that descendedst, Holy Child AfC1 p98
-Gruber Stille Nacht CfC2 p184 (arr. Willcocks), CfC3 p168 (arr. Cashmore)
-Guerrero Canite tuba Adv p49; 3rdCh p5
-Guerrero Gloriose confessor 3rdCh p9
-Hadley I sing of a maiden CfC2 p86
-Halls Hosanna to the Son of David NOEAB p88
-Halls Wash me throughly NOEAB p244
-Händel Ecce quomodo moritur justus Ash p67
-Händel Lord, I trust thee NCAB p228; NOEAB p140; AfC1 p95
-Händel Zadok the Priest NCAB p541
-Handl Ecce concipies Adv p68; 4thCh p9
-Handl Ecce quomodo 4thCh p12
-Handl Resonet in laudibus 4thCh p15
-Hare Thou, O God, art praised in Sion AfC4 p94
-Harris Behold, the tabernacle of God NCAB p58
-Harris Come down, O Love divine NCAB p94
-Harris Faire is the heaven AfC4 p100
-Harris Fear not, O land NOEAB p57
-Harris Holy is the true light NCAB p164
-Harris Most glorious Lord of life OEAB p163; Ash p182
-Harris Vexilla Regis Cunctis (Tarry no longer; toward thine heritage) OEAB p167
-Harris (arr.) O strength and stay AfC1 p156
-Hassler Cantate Domino 4thCh p18
-Hassler Laetentur caeli 4thCh p21
-Hassler Tu es Petrus 4thCh p24
-Hilton Lord, for Thy tender mercy's sake OEAB p27
-Hoddinott Puer natus AfC4 p18
-Holst In the bleak mid-winter CfC3 p93
-Holst Turn back O Man NCAB p488; AfC4 p188
-Holst (arr.) Personent Hodie CfC2 p160
-Hopkins Kings of the Orient CfC3 p190
-How Advent Message NOEAB p2
-How Day by day NOEAB p49
-How Praise, O praise NCAB p359
-Howells Like as the hart AfC4 p158
-Howells My eyes for beauty pine NCAB p235; NOEAB p152; OEAB p169
-Howells Tryste noel CfC3 p172
-Hurford Litany to the Holy Spirit NOEAB p133
-Hurford Sunny bank CfC3 p36
-Hutchings Hosanna to the Son of David Ash p84
-Ingegneri In monte oliveti 1stCh p10
-Ireland Greater love hath no man AfC4 p174
-Isaac Gustate et videte 5thCh p9
-Isaac Ierusalem surge 5thCh p11
-Isom King of all ages, throned on high NOEAB p123
-Ives, G. Ride on Ash p87
-Ives, G. This is the record of John Adv p187
-Jackson I look from afar Adv p101
-Jackson Lift up your heads AfC4 p43
-Jackson Lo, God is here AfC1 p88
-Jackson Tomorrow go ye forth Adv p195
-Jacob O Lord, I will praise Thee OEAB p123
-Jacques I saw three ships CfC1 p56
-Jacques When Christ was born CfC1 p165
-Jacques (arr.) Angels, from the realms of glory CfC1 p16
-Jacques (arr.) Away in a manger CfC1 p3
-Jacques (arr.) Patapan CfC2 p212
-Jacques (arr.) Rejoice and be merry CfC1 p102
-Jacques (arr.) The Holly and the Ivy CfC1 p130
-Jacques (arr.) The linden tree carol CfC1 p110
-John IV Crux fidelis NCAB p112; Ash p136
-Johnson Dum transisset 2ndCh p16
-Josquin des Près Ave Maria 5thCh p13
-Josquin des Près Tu solus 5thCh p21
-Joubert O Lorde, the maker of al thing NCAB p310
-Joubert Torches CfC1 p150
-Kirkpatrick Away in a manger CfC1 p2
-Kocher As with gladness men of old CfC1 p8
-Kodály (arr.) A Christmas Carol CfC1 p18
-Lassus Adoramus te. Christe Ash p69
-Lassus Improperium 5thCh p25
-Lassus Jubilate Deo 5thCh p28
-Lassus Scio enim 5thCh p31
-Lassus Super flumina Babylonis NCAB p425
-Ledger Adam lay ybounden Adv p1
-Ledger Loving Shepherd of thy sheep NOEAB p148
-Ledger (arr.) This joyful Eastertide Ash p186
-Leighton A hymn to the Trinity AfC4 p67
-Leighton Solus ad victimam NCAB p413; AfC1 p13
-Leuner The shepherds' cradle song CfC2 p123
-Ley Come, Thou long expected Jesus OEAB p4
-Ley Lo, round the throne a glorious band NCAB p215
-Ley The strife is o'er NCAB p448
-Ley (arr.) A Choral Hymn for Advent or Ascensiontide) OEAB p68
-Lindley (arr.) Now the green blade riseth Ash p190
-Lloyd Drop down, ye heavens Adv p61
-Lole Jesu, the very thought of thee NOEAB p108
-Loosemore O Lord, increase our faith NCAB p284
-Loosemore The Litany (BCP) Ash p17
-Lord A prayer for peace AfC4 p172
-Lord Most glorious Lord of Lyfe! AfC1 p101
-Lully (attrib.) Far away, what splendour comes this way? NOEAB p54
-Malcolm Ingrediente Domino Ash p92
-Manz E'en so Lord Jesus, Quickly Come Adv p72
-Marchant The souls of the righteous NCAB p443; OEAB p97
-Marenzio O rex gloriae 1stCh p13
-Marenzio Tribus miraculis 1stCh p16
-Marshall The Litany (ASB) Ash p24
-Mathias A Babe is born CfC3 p4
-Mathias Lift up your heads, O ye gates AfC1 p81
-Mathias Make a joyful noise (Jubilate Deo) AfC4 p134
-Mathias Salve regina NCAB p404
-Mathias Sir Christèmas CfC2 p114
-McKie We wait for thy loving kindness AfC4 p77
-Mendelssohn Above all praise NCAB p10; OEAB p74
-Mendelssohn Hark! the herald angels sing CfC1 p39 (with Willcocks descant), CfC3 p68
-Mendelssohn How lovely are the messengers (from Saint Paul) Adv p92
-Mendelssohn Sleepers, wake AfC1 p192
-Mendelssohn When Jesus, our Lord NCAB p512
-Monteverdi Christe, Redemtor omnium CfC3 p49
-Moore Antiphon NCAB p24
-Moore Magnificat in B flat Adv p121
-Morales Peccantem me quotidie Ash p27; 3rdCh p13
-Morales Regina caeli 3rdCh p16
-Morales Simile est regnum 3rdCh p19
-Morgan A Palm Sunday Antiphon NCAB p5
-Morley Agnus Dei Ash p33; 2ndCh p20
-Morley Eheu, sustulerunt Ash p139
-Morley Nolo mortem peccatoris NCAB p259; XVIAB p13
-Mozart Ave verum corpus NCAB p48; NOEAB p14; OEAB p29
-Mozart Grosse Messe Loose; Breitkopf edition
-Mudd Let thy merciful ears, O Lord NCAB p209; OBTA p147
-Mundy O Lord, the maker of all things NCAB p302; OBTA p240
-Near There is no rose Adv p184
-Nicolai (arr. Bach, J.S.) Wachet auf! Adv p211
-Oldroyd (arr.) Ye watchers and ye holy ones OEAB p84
-Ord Adam lay ybounden CfC2 p10
-Ortiz Ianitor caeli 3rdCh p23
-Ouseley From the rising of the sun AfC1 p49
-Ouseley How goodly are thy tents AfC1 p70
-Oxley My shepherd is Lord NCAB p238
-Palestrina Adoramus te, Christe NCAB p14
-Palestrina Alma redemptoris mater 1stCh p20
-Palestrina Benedictus qui venit (from Missa Quarta) XVIAB p28
-Palestrina Come, Thou Holy Spirit, come OEAB p80
-Palestrina Ego sum panis vivus 1stCh p23
-Palestrina Exaltabo te Domine Loose. Chester edition
-Palestrina Fuit homo missus a Deo Adv p79
-Palestrina Matin Responsory Adv p130; CfC2 p68
-Palestrina Missa Brevis Loose. Chester edition
-Palestrina O Bone Iesu (4v) OEAB p104
-Palestrina Salvator mundi NCAB p401
-Palestrina Sanctus (from Missa Quarta) XVIAB p51
-Palestrina Sicut cervus 1stCh p27
-Palestrina Super flumina 1stCh p31
-Palestrina Vesper Responsory Adv p203
-Parry My soul, there is a country NCAB p244
-Parry I was glad when they said unto me Loose. Novello edition
-Parsons Ave Maria OBTA p32
-Pärt Bogoroditsye Dyevo Adv p46
-Pearsall Ave verum corpus NOEAB p18
-Pearsall In dulci jubilo CfC1 p42
-Peeters Ave verum corpus Ash p110
-Pettman (arr.) I saw a maiden CfC2 p83
-Philips Ascendit Deus OBTA p22
-Philips Surgens Jesus NCAB p431
-Piæ Cantiones (arr. Jaques) Good King Wenceslas CfC1 p34
-Piæ Cantiones (arr. Willcocks) Of the Father's heart begotten CfC2 p128
-Piæ Cantiones (arr. Woodward) Up! good Christen folk, and listen CfC1 p157
-Piæ Cantiones arr. Archer Long ago, prophets knew Adv p119
-Piccolo O come, let us sing unto the Lord NCAB p266
-Pitoni Cantate Domino NCAB p92; NOEAB p34; AfC1 p44
-Poston Jesus Christ the Apple Tree Adv p113
-Poston (arr.) The Boar's head carol CfC1 p117
-Praetorius A great and mighty wonder CfC1 p1
-Praetorius Omnis mundis jocundetur CfC3 p144
-Praetorius Psallite unigenito CfC3 p146
-Praetorius Puer natus est nobis 4thCh p28
-Praetorius Salve rex noster 4thCh p29
-Psalmodia Sacra (arr. Willcocks) Bethlehem, of noblest cities CfC3 p40
-Purcell O God the King of glory AfC1 p136
-Purcell Rejoice in the Lord alway NCAB p378
-Purcell Thou knowest, Lord NCAB p463; NOEAB p236
-Purcell, D. I will thank thee, O Lord NOEAB p96
-Rachmaninoff To thee, O Lord AfC1 p203
-Ravenscroft Remember, O thou man Adv p170
-Rawsthorne Like as the hart Ash p37
-Ridout A Pure River of Water of Life AfC4 p63
-Rivaflecha Anima mea 3rdCh p26
-Rowley (arr.) Shepherds loud their praises singing OEAB p15
-Rudolph Jesu, the very thought of thee NOEAB p113
-Rudolph Veiled in darkness Adv p199
-Rutter A Gaelic Blessing NCAB p1
-Rutter Christ the Lord is risen again AfC4 p33; Ash p194
-Rutter Donkey carol CfC3 p55
-Rutter God be in my head NCAB p141
-Rutter Jesus Child CfC3 p74
-Rutter Nativity carol CfC2 p16
-Rutter O clap your hands AfC4 p53
-Rutter Praise ye the Lord AfC1 p184
-Rutter Shepherd's pipe carol CfC2 p39
-Rutter Star carol CfC3 p157
-Rutter The peace of God NOEAB p215
-Rutter Thy perfect love NOEAB p238
-Rutter (arr.) Angel tidings CfC3 p106
-Rutter (arr.) Child in a manger CfC3 p42
-Rutter (arr.) Cradle song CfC3 p112
-Rutter (arr.) Down in yon forest CfC2 p32
-Rutter (arr.) Flemish carol CfC3 p31
-Rutter (arr.) Here we come a-wassailing CfC2 p51
-Rutter (arr.) I saw three ships CfC3 p94
-Rutter (arr.) Il est né le divin enfant CfC2 p74
-Rutter (arr.) In dulci jubilo CfC3 p116
-Rutter (arr.) King Jesus hath a garden CfC3 p123
-Rutter (arr.) Noël nouvelet CfC2 p100
-Rutter (arr.) O come, O come Immanuel Adv p141
-Rutter (arr.) Past three a clock CfC2 p153
-Rutter (arr.) Quem pastores laudavere CfC2 p166
-Rutter (arr.) Quittez, Pasteurs CfC2 p169
-Rutter (arr.) Sans Day Carol CfC2 p107
-Rutter (arr.) The twelve days of Christmas CfC2 p134
-Rutter (arr.) Wexford Carol CfC3 p69
-Saint-Saëns Ave verum corpus NOEAB p21
-Saint-Saëns Panis angelicus NCAB p357
-Sanders The Reproaches Ash p143
-Sargent (arr.) Zither Carol CfC1 p32
-Scheidt A child is born in Bethlehem CfC2 p7
-Scheidt Surrexit Christus hodie Ash p202
-Schein (arr.) A babe is born in Bethlehem CfC3 p15
-Schubert Holy, holy, holy NOEAB p83
-Schubert Where Thou reignest NCAB p523
-Schütz Praise to thee, Lord Jesus NCAB p366
-Scott Easter Anthems Ash p208
-Scott (arr.) I saw water (Vidi aquam) Ash p155
-Scott (arr.) Lent Prose Ash p1
-Scott (arr.) O mortal man Ash p132
-Senfl Deus in adiutorium 4thCh p34
-Shaw Kings in glory OEAB p22
-Shaw (arr.) Coventry Carol CfC1 p82
-Shephard A new commandment Ash p114
-Shephard Never, weather-beaten sail Adv p133
-Shephard Sing, my tongue Ash p115
-Shephard Song of Mary NOEAB p189
-Shephard The Easter Song of Praise Ash p212
-Shephard The secret of Christ NCAB p438
-Shepherd In manus tuas 2ndCh p22
-Somervell O Saviour of the world NCAB p330
-Soriano Regina caeli 1stCh p35
-Stainer God so loved the world NOEAB p81; Ash p72
-Stainer How beautiful upon the mountains Adv p87
-Stanford Benedictus in C Adv p38
-Stanford Glorious and Powerful God NCAB p129
-Stanford Pray that Jerusalem NCAB p372
-Stanford Ye choirs of new Jerusalem AfC1 p215; Ash p216
-Stanford (arr.) O for a closer walk AfC1 p142
-Stanton Alleluia! Hearts to Heaven OEAB p52
-Stanton Christ is the world's true Light OEAB p9
-Statham Drop down, ye heavens OEAB p172
-Sterndale Bennett God is a spirit NCAB p142
-Sterndale Bennett O that I knew where I might find him! NCAB p336
-Stevens (arr.) Sing we to this merry company CfC3 p166
-Stevens (arr.) There is no rose CfC2 p190
-Stewart On this day earth shall ring AfC4 p24
-Stone The Lord's Prayer AfC1 p172
-Sullivan (arr.) It came upon the midnight clear CfC2 p89 (with Willcocks descant), CfC1 p59
-Sweelinck How brightly beams the morning star! NOEAB p90
-Tallis Audivi, media nocte XVIAB p8
-Tallis Euge caeli 2ndCh p25
-Tallis If ye love me NCAB p177; NOEAB p98; OBTA p122
-Tallis O Lord, give thy Holy Spirit XVIAB p47
-Tallis O nata lux OBTA p248
-Tallis Salvator mundi OBTA p273
-Tallis Sancte Deus 2ndCh p27
-Tallis Verily, verily I say unto you AfC1 p208
-Tallis (attrib.) All people that on earth do dwell AfC1 p18
-Tate Carol, with lullaby CfC1 p72
-Taverner Alleluia 2ndCh p33
-Taverner Audivi 2ndCh p35
-Tchaikovsky Holy, Holy, Holy (Hymn to the Trinity) NCAB p155
-Tchaikovsky The crown of roses CfC3 p196
-Terry Myn lyking CfC2 p84
-Terry Richard de Castre's Prayer to Jesus (Jhesu, Lord, that mades me) OEAB p175
-Thatcher Come, ye faithful NCAB p104; NOEAB p44; OEAB p58
-Thorne Christ is our Cornerstone NOEAB p36
-Tomblings All from the sun's uprise OEAB p129
-Tomkins I heard a voice OBTA p126
-Tomkins O pray for the peace of Jerusalem XVIAB p101
-Tomkins When David heard OBTA p332
-Trevor (arr.) The angels and the shepherds CfC2 p182
-Turner O Trinity, most blessed light AfC1 p159
-Tye A sound of angels AfC1 p1
-Tye Give almes of thy goods AfC1 p54; OBTA p67
-Tye Gloria laus 2ndCh p38
-Tye O come, ye servants of the Lord (Laudate nomen Domini) NOEAB p155; AfC1 p120
-Tye O God be merciful XVIAB p88
-Tye O Holy Spirit, Lord of grace NCAB p275
-Tye Sing unto the Lord XVIAB p58
-Vaet O quam gloriosum 5thCh p35
-Vann There is a flow'r sprung of a tree Adv p182
-Vaughan Williams Let us now praise famous men NCAB p212; NOEAB p130
-Vaughan Williams No sad thought his soul affright CfC1 p84
-Vaughan Williams O clap your hands AfC4 p197
-Vaughan Williams O how amiable NCAB p278; OEAB p181; AfC4 p152
-Vaughan Williams O little town of Bethlehem CfC1 p92
-Vaughan Williams O taste and see NOEAB p166; OEAB p106; AfC4 p86
-Vaughan Williams The Blessed son of God CfC1 p112
-Vaughan Williams (arr.) All in the morning CfC3 p122
-Vaughan Williams (arr.) Gloucestershire wassail CfC1 p160
-Vaughan Williams (arr.) This is the truth sent from above CfC2 p202; Adv p194
-Vaughan Williams (arr.) We've been a while a-wandering CfC1 p158
-Viadana Exsultate justi XVIAB p75; 1stCh p37
-Viadana We adore Thee, O Lord Christ OEAB p33
-Victoria Ave Maria 3rdCh p29
-Victoria Genitori genitoque XVIAB p66
-Victoria Jesu dulcis memoria NCAB p181
-Victoria Jesu, the very thought of Thee OEAB p153
-Victoria O magnum mysterium 3rdCh p32
-Victoria O quam gloriosum NCAB p316
-Victoria O vos omnes 3rdCh p36
-Victoria Popule meus Ash p150
-Victoria Pueri Hebraeorum Ash p94; 3rdCh p38
-Wade O come, all ye faithful CfC3 p137
-Wagner O Christ, O blessed Lord AfC1 p117
-Walford Davies Blest are the pure in heart NCAB p62
-Walford Davies God be in my head NCAB p140; NOEAB p76
-Walford Davies O little town of Bethlehem CfC3 p138
-Walford Davies O sons and daughters Ash p225
-Walford Davies (arr.) The holly and the ivy CfC2 p196
-Walmisley Not unto us, O Lord AfC1 p107
-Walter Verbum caro factum est 4thCh p39
-Walton A litany AfC4 p29
-Walton All this time CfC2 p13
-Walton Drop, drop, slow tears Ash p41
-Walton King Herod and the cock CfC3 p186
-Walton Set me as a seal AfC4 p82
-Walton What cheer? CfC1 p162
-Warrell (arr.) A merry Christmas CfC1 p60
-Waters I sing of a Maiden that is mateless OEAB p21
-Waters Virgin-born, we bow before thee NOEAB p242
-Weelkes Alleluia. I heard a voice OBTA p1
-Weelkes Gloria in excelsis Deo OBTA p72
-Weelkes Hosanna to the Son of David OBTA p113
-Weelkes O Lord, arise OBTA p209
-Weelkes When David heard OBTA p343
-Wesley Wash me throughly Ash p45
-Wesley, S. S. Blessed be the God and Father NCAB p64
-Wesley, S. S. Lead me, Lord NCAB p206; NOEAB p127; AfC1 p78
-Wesley, S. S. O Lord my God NCAB p288
-Wesley, S. S. Thou judge of quick and dead NCAB p458
-Wesley, S. S. Thou wilt keep him in perfect peace NCAB p482
-Wesley, S. S. Wash me throughly NCAB p502
-White A Prayer of St. Richard of Chichester OEAB p177
-Whitlock He is risen Ash p229
-Whyte O Christ, who art the light and day AfC1 p118
-Wilby God be in my head NOEAB p77
-Willaert O magnum mysterium 5thCh p38
-Willcocks Birthday carol CfC3 p149
-Willcocks Love divine, all loves excelling NOEAB p143
-Willcocks Unto us is born a son CfC1 p154
-Willcocks (arr.) A child this day is born CfC3 p16
-Willcocks (arr.) Angelus ad virginem CfC3 p26
-Willcocks (arr.) Blessed be that maid Mary CfC1 p23
-Willcocks (arr.) Boar's head carol CfC3 p171
-Willcocks (arr.) Christ was born on Christmas day CfC3 p46
-Willcocks (arr.) Come all you worthy gentlemen CfC3 p52
-Willcocks (arr.) Come, thou redeemer of the earth CfC2 p71
-Willcocks (arr.) Deck the hall CfC2 p22, CfC3 p54 (simpler arrangement)
-Willcocks (arr.) Ding Dong! Merrily on high CfC2 p28
-Willcocks (arr.) Gabriel's message CfC2 p191, CfC3 p170 (simpler arrangement)
-Willcocks (arr.) He smiles within his cradle CfC3 p86
-Willcocks (arr.) How far is it to Bethlehem? CfC2 p66
-Willcocks (arr.) Hush! my dear, lie still and slumber CfC3 p89
-Willcocks (arr.) I saw three ships CfC1 p54
-Willcocks (arr.) Il est né le divin enfant CfC3 p102
-Willcocks (arr.) Infant holy, infant lowly CfC1 p52
-Willcocks (arr.) Lo! he comes with clouds descending CfC3 p133
-Willcocks (arr.) Masters in this hall CfC2 p94
-Willcocks (arr.) O come, all ye faithful CfC1 p88
-Willcocks (arr.) O come, O come Emmanuel CfC2 p120
-Willcocks (arr.) Of the Father's heart begotten AfC1 p166
-Willcocks (arr.) Quelle est cette odeur agréable CfC2 p162
-Willcocks (arr.) Resonemus laudibus CfC2 p177
-Willcocks (arr.) Rocking CfC1 p70
-Willcocks (arr.) Shepherds, in the fields abiding CfC3 p164
-Willcocks (arr.) Sussex Carol CfC1 p96
-Willcocks (arr.) The cherry tree carol CfC2 p92
-Willcocks (arr.) The first Nowell CfC1 p126
-Willcocks (arr.) The infant king CfC2 p188
-Willcocks (arr.) The Lord at first did Adam make CfC2 p198
-Willcocks (arr.) Tomorrow shall be my dancing day CfC2 p203
-Willcocks (arr.) What child is this? CfC3 p187
-Wise Blessed is he that considereth NCAB p77
-Wood Never weather-beaten sail NCAB p253
-Wood O thou, the central orb NCAB p340; AfC4 p9; Adv p149
-Wood Oculi omnium NCAB p349
-Wood (arr.) A virgin most pure CfC1 p14
-Wood (arr.) God rest you merry, gentlemen CfC1 p29
-Wood (arr.) Hail! Blessed Virgin Mary CfC2 p50
-Wood (arr.) Once, as I remember CfC3 p148
-Wood (arr.) Past three a clock CfC1 p101
-Wood (arr.) This joyful Eastertide NOEAB p229; CfC3 p198
-Wood (harm.) Ding Dong! Merrily on high CfC1 p28
-Wood (harm.) King Jesus hath a garden CfC1 p68
\ No newline at end of file
+Composer Title Where Sung
+Aichinger Factus est repente 4thCh p2
+Aichinger Regina caeli 4thCh p7
+Amner Lift up your heads O ye gates XVIAB p41
+Amner O God my King AfC1 p130
+Anerio Alleluia. Christus surrexit Ash p156
+Anerio Christus factus est Ash p52; 1stCh p1 🟢
+Anerio, G. F. Requiem aeternam 1stCh p4
+Anon. Easter Alleluias: (a) Antiphon with psalm tone, (b) Plainchant Alleluia Ash p154 🟢
+Anon. Come, rock the cradle for him CfC3 p53
+Anon. (16th Century) O Lord, the maker of all thing XVIAB p85
+Anon. (16th Century) Rejoice in the Lord alway XVIAB p1; Adv p162 🟢
+Anon. (16th Century) This is the day XVIAB p32
+Arcadelt Haec dies NCAB p146; 5thCh p2
+Arcadelt O Lord, my God, to thee NCAB p293
+Arcadelt (attrib.) Ave Maria NOEAB p12
+Archer Advent Wreath Prayers Adv p16
+Archer And I saw a new heaven NOEAB p6
+Archer Ave Maria Adv p33
+Archer Creator of the stars of night Adv p56
+Archer Prayer for the Blessing of Light Adv p160
+Archer The Linden Tree Carol Adv p180 🟢
+Archer The Lord goes up NOEAB p210
+Archer (arr.) Alma redemptoris mater Adv p22
+Archer (arr.) On Jordan's bank Adv p146
+Archer (arr.) People, look East NOEAB p176
+Archer (arr.) The Angel Gabriel Adv p171
+Armstrong Gibbs Bless the Lord, O my soul OEAB p91
+Armstrong Gibbs O, praise God in His holiness OEAB p112
+Armstrong Gibbs The strife is o'er OEAB p46
+Armstrong Gibbs While the shepherds were watching CfC1 p168
+Arne Help me, O Lord OEAB p133
+Aston I give you a new commandment NOEAB p93
+Aston So they gave their bodies NCAB p416
+Attwood Come, Holy Ghost NCAB p100; NOEAB p40
+Attwood O God, who by the leading of a star AfC1 p123
+Attwood Teach me, O Lord NOEAB p206; AfC1 p196
+Attwood Turn thy face from my sins NCAB p494
+Bach, J.S. All people at this hour OEAB p78
+Bach, J.S. Awake us, Lord, and hasten AfC1 p34
+Bach, J.S. Awake, thou wintry earth NCAB p53
+Bach, J.S. Come sweetest death OEAB p134
+Bach, J.S. Dearest Lord Jesu OEAB p1
+Bach, J.S. Flocks in pastures green abiding OEAB p136
+Bach, J.S. Forget me not OEAB p141
+Bach, J.S. God is living, God is here AfC1 p212
+Bach, J.S. God is our hope and strength AfC1 p59
+Bach, J.S. Here lies He now OEAB p25
+Bach, J.S. Jesu, hope of men despairing OEAB p35
+Bach, J.S. Jesu, joy of man's desiring NCAB p185; NOEAB p101 🟢
+Bach, J.S. Jesu, lead my footsteps ever NCAB p193
+Bach, J.S. King of glory, King of peace NCAB p201
+Bach, J.S. St. Matthew Passion Loose, Novello edition
+Bach, J.S. Subdue us by Thy goodness NCAB p421
+Bach, J.S. Up, up, my heart! with gladness AfC1 p206
+Bach, J.S. Wie soll ich dich empfangen (from The Christmas Oratorio) Adv p213
+Bach, J.S. Ah! dearest Jesu (from The Christmas Oratorio) CfC3 p22
+Bach, J.S. And there were shepherds CfC1 p10
+Bach, J.S. With all thy hosts (from The Christmas Oratorio) CfC3 p22
+Bach, J.S. Zion hört die Wächter singen CfC2 p214 🟢
+Bach, J.S. (harm.) O little one sweet CfC1 p87
+Bain Brother James' Air NOEAB p30
+Bainton A babe is born I wys CfC2 p6
+Bairstow I sat down under his shadow AfC1 p74 🟢
+Bairstow Jesu, the very thought of thee NCAB p197
+Bairstow Let all mortal flesh keep silence AfC4 p88
+Bairstow Psalm 114 Ash p165
+Bairstow The day draws on with golden light NCAB p436
+Bairstow The Lamentation Ash p55
+Bairstow Though I speak with the tongues of men NCAB p484
+Bairstow (after Gibbons) Jesu, grant me this I pray Ash p60
+Ballet Lute-book lullaby CfC1 p108
+Barcrofte O almighty God AfC1 p112
+Barnard (arr.) In the heart where love is abiding Ash p100
+Batten Deliver us, O Lord our God XVIAB p99
+Batten Haste thee, O God AfC1 p64
+Batten Let my complaint come before thee XVIAB p24
+Batten Lord, we beseech thee XVIAB p20
+Batten O praise the Lord OBTA p251
+Batten O sing joyfully XVIAB p70 🟢
+Batten When the Lord turned again XVIAB p35
+Bax Lord, thou hast told us AfC4 p28
+Bennett Out of your sleep CfC2 p150
+Bennett Susanni CfC3 p18
+Bennett What sweeter music CfC3 p192
+Berkeley I sing of a maiden Adv p109
+Berlioz The Shepherd's farewell CfC1 p142
+Berry (arr.) Advent Antiphons (Latin) Adv p8
+Bevan There's a wideness in God's mercy NOEAB p224
+Bevan (arr.) O Thou who at Thy Eucharist did'st pray OEAB p99
+Bevan (arr) O love of whom is truth and light OEAB p144
+Blackwell (arr.) O Thou, whose all-redeeming might NOEAB p168
+Blow Let my prayer AfC1 p86
+Blow Praise the Lord, ye servants AfC1 p174
+Bohemian Brethren (arr. Guest) Zion, at thy shining gates Adv p214
+Bourgeois O gladsome light, O grace NCAB p273
+Bourgeois O strength and stay AfC1 p156
+Bourne Thou art God NOEAB p231
+Brahms Ah, thou poor world AfC1 p10
+Britten A boy was born CfC1 p4
+Britten A new year carol CfC2 p64
+Britten Corpus Christi Carrol Loose. Oxford Edition. 🟢
+Britten O be joyful in the Lord (Jubilate Deo) AfC4 p140
+Britten There is no rose CfC3 p181
+Bruckner Locus iste NCAB p222 🟢
+Bruckner Pange lingua (Of the glorious Body telling) Ash p104
+Bruckner Virga Jesse floruit Adv p204
+Bull In the departure of the Lord Ash p123
+Bullard For all thy saints NOEAB p65
+Bullard Praise ye the Lord NOEAB p180
+Bullard Star of the East NOEAB p198
+Bullard The Feast of Palms Ash p74
+Bullock Give us the wings of faith AfC4 p128
+Bullock Good Christian men rejoice and sing OEAB p38
+Bullock (arr.) Give laud unto the Lord OEAB p64
+Byrd Ave verum corpus NCAB p38; OBTA p44; 2ndCh p2 🟢
+Byrd Cibavit eos 2ndCh p6
+Byrd Civitas sancti tui Ash p4 🟢
+Byrd Haec dies OBTA p84 🟢
+Byrd Justorum animae OBTA p131
+Byrd Laetentur coeli OBTA p137
+Byrd Mass for five voices Loose. Chester edition 🟢
+Byrd Miserere mei OBTA p157
+Byrd O quam gloriosum OBTA p256
+Byrd Sacerdotes Domini NCAB p399; XVIAB p55
+Byrd Senex puerum 2ndCh p10
+Byrd Sing joyfully OBTA p287 🟢
+Byrd Teach me, O Lord OBTA p298
+Byrd This day Christ was born OBTA p307
+Byrd Venite comedite 2ndCh p13
+Campbell (arr.) Praise to God in the highest AfC1 p179
+Carter For the beauty of the earth NOEAB p70
+Carter Holy Spirit, truth divine NOEAB p84
+Carter Mary's Magnificat NCAB p231
+Carter O Lord, open thou our lips NCAB p295
+Carter (arr.) Angelus ad Virginem Adv p24 🟢
+Carter (arr.) Joy is come NOEAB p116; Ash p167
+Cashmore (after Praetorius) Es ist ein Ros' entsprungen 74Adv p
+Charpentier Salve puerule CfC3 p154
+Chilcott Be thou my vision NOEAB p23
+Chilcott God so loved the world Ash p64
+Chilcott Nova! nova! Adv p137
+Chilcott (arr.) Were you there? Ash p126
+Clarke-Whitfeld Behold, how good and joyful AfC1 p38
+Clemens non Papa Crux fidelis 5thCh p5
+Cleobury (arr.) Advent Antiphons (English) Adv p3 🟢
+Cleobury (arr.) Advent Prose (English) Adv p11 🟢
+Cleobury (arr.) Advent Prose (Latin) Adv p14 🟢
+Cleobury (arr.) Come, thou Redeemer of the earth Adv p54
+Cleobury (arr.) Let all mortal flesh keep silence Adv p115
+Cleobury (arr.) Man, assay Adv p127
+Cleobury (arr.) The Cherry Tree Carol Adv p174
+Coleman (arr.) Ye servants of God OEAB p108
+Cooke O men from the fields CfC1 p94
+Cope He is risen OEAB p42
+Cope Pleasure it is OEAB p88
+Cornelius The Three Kings CfC1 p136 🟢
+Corrêa O vos omnes NOEAB p174; AfC1 p163
+Croce O sacrum convivium 1stCh p6
+Croce O vos omnes Ash p129
+Crotch Be peace on earth OEAB p147
+Crotch Comfort, O Lord, the soul of thy servant NCAB p110
+Darke Communion Service in F Loose. Oxford Edition. 🟢
+Darlington (arr.) Jacob's Ladder Adv p110
+de Séverac Tantum ergo Ash p108
+Dering Above Him stood the Seraphim OEAB p155
+Dering Factum est silentium OBTA p57
+Dowland He that is down needs fear no fall OEAB p160
+Dowland My spirit longs for Thee OEAB p102
+Drayton Jesu dulcis memoria AfC4 p166
+Drese Round me falls the night NCAB p381
+Ebeling All my heart this night rejoices CfC2 p12
+Eccard When to the temple Mary went NCAB p516
+Elgar Ave verum corpus NCAB p44 🟢
+Elgar Dream of Gerontius Loose. 1900 Novello edition
+Elgar Light of the World Ash p170
+Elgar O salutaris Hostia No. 3 NOEAB p157
+Ellis There is no rose NOEAB p221 🟢
+Esquivel Ego sum panis vivus 3rdCh p2
+Este's Psalter While shepherds watched their flocks by night CfC1 p166 (arr. Ravenscroft), CfC2 p210 (arr. Willcocks) 🟢
+Farrant Call to remembrance NCAB p87; OBTA p50 🟢
+Farrant Hide not thou thy face NCAB p151; OBTA p94 🟢
+Farrant (attrib.) Lord, for thy tender mercy's sake NOEAB p138; NCAB p224; OBTA p152; Ash p13 🟢
+Farrar Almighty God, the fountain of all wisdom AfC1 p24
+Ferguson (arr.) People look East Adv p157
+Ford Almighty God, which hast me brought NCAB p21; AfC1 p28
+Foster Christ the Lord is risen again! NOEAB p39
+Gardiner Evening Hymn NCAB p120
+Gauntlett Once in royal David's city CfC1 p100 (arr. Mann), CfC2 p148 (arr. Mann and Willcocks) 🟢
+Gesius Hosianna dem Sohne Davids Ash p82 🟢
+Gibbons Almighty and everlasting God NCAB p18; OBTA p15 🟢
+Gibbons Drop, drop, slow tears NOEAB p52; NCAB p116 🟢
+Gibbons Hosanna to the Son of David OBTA p99
+Gibbons O clap your hands OBTA p164
+Gibbons O Lord, in thy wrath OBTA p231
+Gibbons Song 44 AfC1 p46
+Gibbons Song 46 AfC1 p30
+Gibbons This is the record of John NCAB p454; OBTA p318 🟢
+Gilbert Let all the world OEAB p119
+Goldschmidt A tender shoot Adv p31
+Goss God so loved the world NCAB p145
+Goss If we believe NCAB p168
+Goss O pray for the peace of Jerusalem AfC1 p146
+Goss O Saviour of the world NCAB p323; NOEAB p163 🟢
+Goss See amid the winter's snow CfC1 p103
+Goss These are they which follow the Lamb AfC1 p200
+Greene Thou visitest the earth NCAB p473 🟢
+Gritton Lord that descendedst, Holy Child AfC1 p98
+Gruber Stille Nacht CfC2 p184 (arr. Willcocks), CfC3 p168 (arr. Cashmore) 🟢
+Guerrero Canite tuba Adv p49; 3rdCh p5
+Guerrero Gloriose confessor 3rdCh p9
+Hadley I sing of a maiden CfC2 p86
+Halls Hosanna to the Son of David NOEAB p88
+Halls Wash me throughly NOEAB p244
+Händel Ecce quomodo moritur justus Ash p67
+Händel Lord, I trust thee NCAB p228; NOEAB p140; AfC1 p95
+Händel Zadok the Priest NCAB p541 🟢
+Handl Ecce concipies Adv p68; 4thCh p9
+Handl Ecce quomodo 4thCh p12
+Handl Resonet in laudibus 4thCh p15
+Hare Thou, O God, art praised in Sion AfC4 p94
+Harris Behold, the tabernacle of God NCAB p58
+Harris Come down, O Love divine NCAB p94
+Harris Faire is the heaven AfC4 p100
+Harris Fear not, O land NOEAB p57
+Harris Holy is the true light NCAB p164
+Harris Most glorious Lord of life OEAB p163; Ash p182
+Harris Vexilla Regis Cunctis (Tarry no longer; toward thine heritage) OEAB p167
+Harris (arr.) O strength and stay AfC1 p156
+Hassler Cantate Domino 4thCh p18 🟢
+Hassler Laetentur caeli 4thCh p21
+Hassler Tu es Petrus 4thCh p24
+Hilton Lord, for Thy tender mercy's sake OEAB p27
+Hoddinott Puer natus AfC4 p18
+Holst In the bleak mid-winter CfC3 p93 🟢
+Holst Turn back O Man NCAB p488; AfC4 p188 🟢
+Holst (arr.) Personent Hodie CfC2 p160
+Hopkins Kings of the Orient CfC3 p190
+How Advent Message NOEAB p2
+How Day by day NOEAB p49 🟢
+How Praise, O praise NCAB p359
+Howells Like as the hart AfC4 p158 🟢
+Howells My eyes for beauty pine NCAB p235; NOEAB p152; OEAB p169 🟢
+Howells Tryste noel CfC3 p172
+Hurford Litany to the Holy Spirit NOEAB p133
+Hurford Sunny bank CfC3 p36
+Hutchings Hosanna to the Son of David Ash p84
+Ingegneri In monte oliveti 1stCh p10
+Ireland Greater love hath no man AfC4 p174 🟢
+Isaac Gustate et videte 5thCh p9
+Isaac Ierusalem surge 5thCh p11
+Isom King of all ages, throned on high NOEAB p123 🟢
+Ives, G. Ride on Ash p87
+Ives, G. This is the record of John Adv p187
+Jackson I look from afar Adv p101
+Jackson Lift up your heads AfC4 p43
+Jackson Lo, God is here AfC1 p88
+Jackson Tomorrow go ye forth Adv p195
+Jacob O Lord, I will praise Thee OEAB p123
+Jacques I saw three ships CfC1 p56
+Jacques When Christ was born CfC1 p165
+Jacques (arr.) Angels, from the realms of glory CfC1 p16
+Jacques (arr.) Away in a manger CfC1 p3 🟢
+Jacques (arr.) Patapan CfC2 p212
+Jacques (arr.) Rejoice and be merry CfC1 p102
+Jacques (arr.) The Holly and the Ivy CfC1 p130 🟢
+Jacques (arr.) The linden tree carol CfC1 p110
+John IV Crux fidelis NCAB p112; Ash p136 🟢
+Johnson Dum transisset 2ndCh p16
+Josquin des Près Ave Maria 5thCh p13 🟢
+Josquin des Près Tu solus 5thCh p21
+Joubert O Lorde, the maker of al thing NCAB p310
+Joubert Torches CfC1 p150
+Kirkpatrick Away in a manger CfC1 p2
+Kocher As with gladness men of old CfC1 p8
+Kodály (arr.) A Christmas Carol CfC1 p18
+Lassus Adoramus te. Christe Ash p69 🟢
+Lassus Improperium 5thCh p25
+Lassus Jubilate Deo 5thCh p28
+Lassus Scio enim 5thCh p31
+Lassus Super flumina Babylonis NCAB p431
+Ledger Adam lay ybounden Adv p1
+Ledger Loving Shepherd of thy sheep NOEAB p148
+Ledger (arr.) This joyful Eastertide Ash p186
+Leighton A hymn to the Trinity AfC4 p67
+Leighton Solus ad victimam NCAB p413; AfC1 p13
+Leuner The shepherds' cradle song CfC2 p123
+Ley Come, Thou long expected Jesus OEAB p4
+Ley Lo, round the throne a glorious band NCAB p215 🟢
+Ley The strife is o'er NCAB p448
+Ley (arr.) A Choral Hymn for Advent or Ascensiontide) OEAB p68
+Lindley (arr.) Now the green blade riseth Ash p190
+Lloyd Drop down, ye heavens Adv p61
+Lole Jesu, the very thought of thee NOEAB p108
+Loosemore O Lord, increase our faith NCAB p284
+Loosemore The Litany (BCP) Ash p17 🟢
+Lord A prayer for peace AfC4 p172
+Lord Most glorious Lord of Lyfe! AfC1 p101
+Lully (attrib.) Far away, what splendour comes this way? NOEAB p54
+Malcolm Ingrediente Domino Ash p92
+Manz E'en so Lord Jesus, Quickly Come Adv p72
+Marchant The souls of the righteous NCAB p443; OEAB p97
+Marenzio O rex gloriae 1stCh p13
+Marenzio Tribus miraculis 1stCh p16
+Marshall The Litany (ASB) Ash p24
+Mathias A Babe is born CfC3 p4
+Mathias Lift up your heads, O ye gates AfC1 p81 🟢
+Mathias Make a joyful noise (Jubilate Deo) AfC4 p134
+Mathias Salve regina NCAB p404
+Mathias Sir Christèmas CfC2 p114
+McKie We wait for thy loving kindness AfC4 p77 🟢
+Mendelssohn Above all praise NCAB p10; OEAB p74
+Mendelssohn Hark! the herald angels sing CfC1 p39 (with Willcocks descant), CfC3 p68 🟢
+Mendelssohn How lovely are the messengers (from Saint Paul) Adv p92
+Mendelssohn Sleepers, wake AfC1 p192
+Mendelssohn When Jesus, our Lord NCAB p512
+Monteverdi Christe, Redemptor omnium CfC3 p49
+Moore Antiphon NCAB p24
+Moore Magnificat in B flat Adv p121
+Morales Peccantem me quotidie Ash p27; 3rdCh p13
+Morales Regina caeli 3rdCh p16
+Morales Simile est regnum 3rdCh p19
+Morgan A Palm Sunday Antiphon NCAB p5
+Morley Agnus Dei Ash p33; 2ndCh p20
+Morley Eheu, sustulerunt Ash p139
+Morley Nolo mortem peccatoris NCAB p259; XVIAB p13 🟢
+Mozart Ave verum corpus NCAB p48; NOEAB p14; OEAB p29 🟢
+Mozart Grosse Messe Loose; Breitkopf edition
+Mudd Let thy merciful ears, O Lord NCAB p209; OBTA p147
+Mundy O Lord, the maker of all things NCAB p302; OBTA p240
+Near There is no rose Adv p184 🟢
+Nicolai (arr. Bach, J.S.) Wachet auf! Adv p211 🟢
+Oldroyd (arr.) Ye watchers and ye holy ones OEAB p84
+Ord Adam lay ybounden CfC2 p10 🟢
+Ortiz Ianitor caeli 3rdCh p23
+Ouseley From the rising of the sun AfC1 p49
+Ouseley How goodly are thy tents AfC1 p70
+Oxley My shepherd is Lord NCAB p238
+Palestrina Adoramus te, Christe NCAB p14 🟢
+Palestrina Alma redemptoris mater 1stCh p20 🟢
+Palestrina Benedictus qui venit (from Missa Quarta) XVIAB p28
+Palestrina Come, Thou Holy Spirit, come OEAB p80
+Palestrina Ego sum panis vivus 1stCh p23 🟢
+Palestrina Exaltabo te Domine Loose. Chester edition
+Palestrina Fuit homo missus a Deo Adv p79
+Palestrina Matin Responsory Adv p130; CfC2 p68 🟢
+Palestrina Missa Brevis Loose. Chester edition 🟢
+Palestrina O Bone Iesu (4v) OEAB p104 🟢
+Palestrina Salvator mundi NCAB p401
+Palestrina Sanctus (from Missa Quarta) XVIAB p51
+Palestrina Sicut cervus 1stCh p27 🟢
+Palestrina Super flumina 1stCh p31 🟢
+Palestrina Vesper Responsory Adv p203 🟢
+Parry My soul, there is a country NCAB p244 🟢
+Parry I was glad when they said unto me Loose. Novello edition 🟢
+Parsons Ave Maria OBTA p32 🟢
+Pärt Bogoroditsye Dyevo Adv p46
+Pearsall Ave verum corpus NOEAB p18
+Pearsall In dulci jubilo CfC1 p42 🟢
+Peeters Ave verum corpus Ash p110
+Pettman (arr.) I saw a maiden CfC2 p83
+Philips Ascendit Deus OBTA p22 🟢
+Philips Surgens Jesus NCAB p431
+Piæ Cantiones (arr. Jaques) Good King Wenceslas CfC1 p34
+Piæ Cantiones (arr. Willcocks) Of the Father's heart begotten CfC2 p128
+Piæ Cantiones (arr. Woodward) Up! good Christen folk, and listen CfC1 p157
+Piæ Cantiones arr. Archer Long ago, prophets knew Adv p119
+Piccolo O come, let us sing unto the Lord NCAB p266
+Pitoni Cantate Domino NCAB p92; NOEAB p34; AfC1 p44 🟢
+Poston Jesus Christ the Apple Tree Adv p113 🟢
+Poston (arr.) The Boar's head carol CfC1 p117
+Praetorius A great and mighty wonder CfC1 p1 🟢
+Praetorius Omnis mundis jocundetur CfC3 p144
+Praetorius Psallite unigenito CfC3 p146
+Praetorius Puer natus est nobis 4thCh p28
+Praetorius Salve rex noster 4thCh p29
+Psalmodia Sacra (arr. Willcocks) Bethlehem, of noblest cities CfC3 p40
+Purcell O God the King of glory AfC1 p136
+Purcell Rejoice in the Lord alway NCAB p381
+Purcell Thou knowest, Lord NCAB p463; NOEAB p236 🟢
+Purcell, D. I will thank thee, O Lord NOEAB p96
+Rachmaninoff To thee, O Lord AfC1 p203
+Ravenscroft Remember, O thou man Adv p170
+Rawsthorne Like as the hart Ash p37
+Ridout A Pure River of Water of Life AfC4 p63
+Rivaflecha Anima mea 3rdCh p26
+Rowley (arr.) Shepherds loud their praises singing OEAB p15
+Rudolph Jesu, the very thought of thee NOEAB p113
+Rudolph Veiled in darkness Adv p199
+Rutter A Gaelic Blessing NCAB p1 🟢
+Rutter Christ the Lord is risen again AfC4 p33; Ash p194
+Rutter Donkey carol CfC3 p55
+Rutter God be in my head NCAB p141
+Rutter Jesus Child CfC3 p74
+Rutter Nativity carol CfC2 p16
+Rutter O clap your hands AfC4 p53 🟢
+Rutter Praise ye the Lord AfC1 p184
+Rutter Shepherd's pipe carol CfC2 p39 🟢
+Rutter Star carol CfC3 p157
+Rutter The peace of God NOEAB p215
+Rutter Thy perfect love NOEAB p238
+Rutter (arr.) Angel tidings CfC3 p106
+Rutter (arr.) Child in a manger CfC3 p42
+Rutter (arr.) Cradle song CfC3 p112
+Rutter (arr.) Down in yon forest CfC2 p32
+Rutter (arr.) Flemish carol CfC3 p31
+Rutter (arr.) Here we come a-wassailing CfC2 p51 🟢
+Rutter (arr.) I saw three ships CfC3 p94 🟢
+Rutter (arr.) Il est né le divin enfant CfC2 p74 🟢
+Rutter (arr.) In dulci jubilo CfC3 p116
+Rutter (arr.) King Jesus hath a garden CfC3 p123
+Rutter (arr.) Noël nouvelet CfC2 p100
+Rutter (arr.) O come, O come Immanuel Adv p141
+Rutter (arr.) Past three a clock CfC2 p153 🟢
+Rutter (arr.) Quem pastores laudavere CfC2 p166
+Rutter (arr.) Quittez, Pasteurs CfC2 p169
+Rutter (arr.) Sans Day Carol CfC2 p107
+Rutter (arr.) The twelve days of Christmas CfC2 p134
+Rutter (arr.) Wexford Carol CfC3 p69 🟢
+Saint-Saëns Ave verum corpus NOEAB p21
+Saint-Saëns Panis angelicus NCAB p357
+Sanders The Reproaches Ash p143
+Sargent (arr.) Zither Carol CfC1 p32
+Scheidt A child is born in Bethlehem CfC2 p7
+Scheidt Surrexit Christus hodie Ash p202
+Schein (arr.) A babe is born in Bethlehem CfC3 p15
+Schubert Holy, holy, holy NOEAB p83
+Schubert Where Thou reignest NCAB p523
+Schütz Praise to thee, Lord Jesus NCAB p366
+Scott Easter Anthems Ash p208
+Scott (arr.) I saw water (Vidi aquam) Ash p155
+Scott (arr.) Lent Prose Ash p1
+Scott (arr.) O mortal man Ash p132
+Senfl Deus in adiutorium 4thCh p34
+Shaw Kings in glory OEAB p22
+Shaw (arr.) Coventry Carol CfC1 p82 🟢
+Shephard A new commandment Ash p114
+Shephard Never, weather-beaten sail Adv p133
+Shephard Sing, my tongue Ash p115
+Shephard Song of Mary NOEAB p189 🟢
+Shephard The Easter Song of Praise Ash p212
+Shephard The secret of Christ NCAB p438
+Shepherd In manus tuas 2ndCh p22
+Somervell O Saviour of the world NCAB p330
+Soriano Regina caeli 1stCh p35
+Stainer God so loved the world NOEAB p81; Ash p72 🟢
+Stainer How beautiful upon the mountains Adv p87
+Stanford Benedictus in C Adv p38
+Stanford Glorious and Powerful God NCAB p129
+Stanford Pray that Jerusalem NCAB p372
+Stanford Ye choirs of new Jerusalem AfC1 p215; Ash p216 🟢
+Stanford (arr.) O for a closer walk AfC1 p142
+Stanton Alleluia! Hearts to Heaven OEAB p52
+Stanton Christ is the world's true Light OEAB p9
+Statham Drop down, ye heavens OEAB p172
+Sterndale Bennett God is a spirit NCAB p142
+Sterndale Bennett O that I knew where I might find him! NCAB p336
+Stevens (arr.) Sing we to this merry company CfC3 p166
+Stevens (arr.) There is no rose CfC2 p190 🟢
+Stewart On this day earth shall ring AfC4 p24
+Stone The Lord's Prayer AfC1 p172
+Sullivan (arr.) It came upon the midnight clear CfC2 p89 (with Willcocks descant), CfC1 p59
+Sweelinck How brightly beams the morning star! NOEAB p90 🟢
+Tallis A new commandment FaberTal p9 🟢
+Tallis Audivi, media nocte XVIAB p8
+Tallis Discomfit them, O Lord FaberTal p24
+Tallis Euge caeli 2ndCh p25
+Tallis I call and cry to thee, O Lord FaberTal p13
+Tallis If ye love me NCAB p177; NOEAB p98; OBTA p122; FaberTal p4 🟢
+Tallis O Lord, give thy Holy Spirit XVIAB p47; FaberTal p11 🟢
+Tallis O nata lux OBTA p248 🟢
+Tallis Hear the voice and prayer FaberTal p6 🟢
+Tallis Salvator mundi OBTA p273 🟢
+Tallis Sancte Deus 2ndCh p27
+Tallis Verily, verily I say unto you AfC1 p208 🟢
+Tallis Why fumeth in sight FaberTal p13
+Tallis With all our heart FaberTal p21
+Tallis (attrib.) All people that on earth do dwell AfC1 p18
+Tate Carol, with lullaby CfC1 p72
+Taverner Alleluia 2ndCh p33
+Taverner Audivi 2ndCh p35
+Tchaikovsky Holy, Holy, Holy (Hymn to the Trinity) NCAB p155
+Tchaikovsky The crown of roses CfC3 p196
+Terry Myn lyking CfC2 p84
+Terry Richard de Castre's Prayer to Jesus (Jhesu, Lord, that mades me) OEAB p175
+Thatcher Come, ye faithful NCAB p104; NOEAB p44; OEAB p58
+Thorne Christ is our Cornerstone NOEAB p36
+Tomblings All from the sun's uprise OEAB p129
+Tomkins I heard a voice OBTA p126
+Tomkins O pray for the peace of Jerusalem XVIAB p101
+Tomkins When David heard OBTA p332
+Trevor (arr.) The angels and the shepherds CfC2 p182
+Turner O Trinity, most blessed light AfC1 p159
+Tye A sound of angels AfC1 p1
+Tye Give almes of thy goods AfC1 p54; OBTA p67
+Tye Gloria laus 2ndCh p38
+Tye O come, ye servants of the Lord (Laudate nomen Domini) NOEAB p155; AfC1 p120
+Tye O God be merciful XVIAB p88
+Tye O Holy Spirit, Lord of grace NCAB p275
+Tye Sing unto the Lord XVIAB p58
+Vaet O quam gloriosum 5thCh p35
+Vann There is a flow'r sprung of a tree Adv p182
+Vaughan Williams Let us now praise famous men NCAB p212; NOEAB p130
+Vaughan Williams No sad thought his soul affright CfC1 p84
+Vaughan Williams O clap your hands AfC4 p197
+Vaughan Williams O how amiable NCAB p278; OEAB p181; AfC4 p152 🟢
+Vaughan Williams O little town of Bethlehem CfC1 p92 🟢
+Vaughan Williams O taste and see NOEAB p166; OEAB p106; AfC4 p86 🟢
+Vaughan Williams The Blessed son of God CfC1 p112
+Vaughan Williams (arr.) All in the morning CfC3 p122
+Vaughan Williams (arr.) Gloucestershire wassail CfC1 p160 🟢
+Vaughan Williams (arr.) This is the truth sent from above CfC2 p202; Adv p194 🟢
+Vaughan Williams (arr.) We've been a while a-wandering CfC1 p158
+Viadana Exsultate justi XVIAB p75; 1stCh p37
+Viadana We adore Thee, O Lord Christ OEAB p33
+Victoria Ave Maria 3rdCh p29 🟢
+Victoria Genitori genitoque XVIAB p66 🟢
+Victoria Jesu dulcis memoria NCAB p181 🟢
+Victoria Jesu, the very thought of Thee OEAB p153
+Victoria O magnum mysterium 3rdCh p32 🟢
+Victoria O quam gloriosum NCAB p316 🟢
+Victoria O vos omnes 3rdCh p36 🟢
+Victoria Popule meus Ash p150
+Victoria Pueri Hebraeorum Ash p94; 3rdCh p38 🟢
+Wade O come, all ye faithful CfC3 p137
+Wagner O Christ, O blessed Lord AfC1 p117
+Walford Davies Blest are the pure in heart NCAB p62
+Walford Davies God be in my head NCAB p140; NOEAB p76
+Walford Davies O little town of Bethlehem CfC3 p138 🟢
+Walford Davies O sons and daughters Ash p225
+Walford Davies (arr.) The holly and the ivy CfC2 p196 🟢
+Walmisley Not unto us, O Lord AfC1 p107
+Walter Verbum caro factum est 4thCh p39
+Walton A litany AfC4 p29
+Walton All this time CfC2 p13
+Walton Drop, drop, slow tears Ash p41
+Walton King Herod and the cock CfC3 p186
+Walton Set me as a seal AfC4 p82
+Walton What cheer? CfC1 p162
+Warrell (arr.) A merry Christmas CfC1 p60
+Waters I sing of a Maiden that is mateless OEAB p21 🟢
+Waters Virgin-born, we bow before thee NOEAB p242
+Weelkes Alleluia. I heard a voice OBTA p1
+Weelkes Gloria in excelsis Deo OBTA p72
+Weelkes Hosanna to the Son of David OBTA p113 🟢
+Weelkes O Lord, arise OBTA p209
+Weelkes When David heard OBTA p343 🟢
+Wesley, S. S. Blessed be the God and Father NCAB p64 🟢
+Wesley, S. S. Lead me, Lord NCAB p206; NOEAB p127; AfC1 p78 🟢
+Wesley, S. S. O Lord my God NCAB p288
+Wesley, S. S. Thou judge of quick and dead NCAB p458
+Wesley, S. S. Thou wilt keep him in perfect peace NCAB p482 🟢
+Wesley, S. S. Wash me throughly NCAB p502; Ash p45
+White A Prayer of St. Richard of Chichester OEAB p177
+Whitlock He is risen Ash p229
+Whyte O Christ, who art the light and day AfC1 p118
+Wilby God be in my head NOEAB p77
+Willaert O magnum mysterium 5thCh p38
+Willcocks Birthday carol CfC3 p149
+Willcocks Love divine, all loves excelling NOEAB p143 🟢
+Willcocks Unto us is born a son CfC1 p154
+Willcocks (arr.) A child this day is born CfC3 p16
+Willcocks (arr.) Angelus ad virginem CfC3 p26 🟢
+Willcocks (arr.) Blessed be that maid Mary CfC1 p23
+Willcocks (arr.) Boar's head carol CfC3 p171
+Willcocks (arr.) Christ was born on Christmas day CfC3 p46
+Willcocks (arr.) Come all you worthy gentlemen CfC3 p52 🟢
+Willcocks (arr.) Come, thou redeemer of the earth CfC2 p71 🟢
+Willcocks (arr.) Deck the hall CfC2 p22, CfC3 p54 (simpler arrangement) 🟢
+Willcocks (arr.) Ding Dong! Merrily on high CfC2 p28 🟢
+Willcocks (arr.) Gabriel's message CfC2 p191, CfC3 p170 (simpler arrangement) 🟢
+Willcocks (arr.) He smiles within his cradle CfC3 p86
+Willcocks (arr.) How far is it to Bethlehem? CfC2 p66
+Willcocks (arr.) Hush! my dear, lie still and slumber CfC3 p89
+Willcocks (arr.) I saw three ships CfC1 p54
+Willcocks (arr.) Il est né le divin enfant CfC3 p102 🟢
+Willcocks (arr.) Infant holy, infant lowly CfC1 p52
+Willcocks (arr.) Lo! he comes with clouds descending CfC3 p133
+Willcocks (arr.) Masters in this hall CfC2 p94
+Willcocks (arr.) O come, all ye faithful CfC1 p88 🟢
+Willcocks (arr.) O come, O come Emmanuel CfC2 p120 🟢
+Willcocks (arr.) Of the Father's heart begotten AfC1 p166
+Willcocks (arr.) Quelle est cette odeur agréable CfC2 p162
+Willcocks (arr.) Resonemus laudibus CfC2 p177
+Willcocks (arr.) Rocking CfC1 p70
+Willcocks (arr.) Shepherds, in the fields abiding CfC3 p164
+Willcocks (arr.) Sussex Carol CfC1 p96 🟢
+Willcocks (arr.) The cherry tree carol CfC2 p92
+Willcocks (arr.) The first Nowell CfC1 p126 🟢
+Willcocks (arr.) The infant king CfC2 p188
+Willcocks (arr.) The Lord at first did Adam make CfC2 p198
+Willcocks (arr.) Tomorrow shall be my dancing day CfC2 p203
+Willcocks (arr.) What child is this? CfC3 p187
+Wise Blessed is he that considereth NCAB p77
+Wood Never weather-beaten sail NCAB p253
+Wood O thou, the central orb NCAB p340; AfC4 p9; Adv p149 🟢
+Wood Oculi omnium NCAB p349
+Wood (arr.) A virgin most pure CfC1 p14
+Wood (arr.) God rest you merry, gentlemen CfC1 p29
+Wood (arr.) Hail! Blessed Virgin Mary CfC2 p50
+Wood (arr.) Once, as I remember CfC3 p148
+Wood (arr.) Past three a clock CfC1 p101
+Wood (arr.) This joyful Eastertide NOEAB p229; CfC3 p198 🟢
+Wood (harm.) King Jesus hath a garden CfC1 p68
+Wood (harm.) Ding Dong! Merrily on high CfC1 p28 🟢
diff --git a/trees/isa-0002.tree b/trees/isa-0002.tree
new file mode 100644
index 0000000..80ccc92
--- /dev/null
+++ b/trees/isa-0002.tree
@@ -0,0 +1,295 @@
+\date{2025-11-25}
+\author{liamoc}
+\title{Natural Deduction}
+\taxon{Lecture}
+\import{shiki-macros}
+\put\shiki/language{Isabelle Theory}
+
+\transclude{isa-0003}
+
+\shiki{theory ND
+ imports Pure
+begin
+
+typedecl bool
+judgment Trueprop :: "bool ⇒ prop" (‹(_)› 5)
+}
+
+
+
+\shiki{axiomatization
+ conj :: "bool ⇒ bool ⇒ bool" (infixr "∧" 35) and
+where
+ (* Conjunction *)
+ conjI : "⟦ A ; B ⟧ ⟹ (A ∧ B)" and
+ conjunct1 : "A ∧ B ⟹ A" and
+ conjunct2 : "A ∧ B ⟹ B"
+}
+
+\shiki{
+ disj :: "bool ⇒ bool ⇒ bool" (infixr "∨" 30) and
+ implies :: "bool ⇒ bool ⇒ bool" (infixr "⟶" 25) and
+ not :: "bool ⇒ bool" ("¬ _" [40] 40)
+
+ (* Disjunction *)
+ disjI1 : "A ⟹ (A ∨ B)" and
+ disjI2 : "B ⟹ (A ∨ B)" and
+ disjE : "⟦ A ∨ B ; A ⟹ C ; B ⟹ C ⟧ ⟹ C" and
+
+ (* Implication *)
+ impI : "(A ⟹ B) ⟹ (A ⟶ B)" and
+ mp : "⟦ A ⟶ B ; A ⟧ ⟹ B" and
+
+ (* Negation *)
+ notI : "(A ⟹ False) ⟹ ¬ A" and
+ notE : "⟦ ¬ A ; A ⟧ ⟹ R" and
+
+ (* False and True *)
+ FalseE : "False ⟹ C" and
+ TrueI : "True"
+
+lemma conjE : ‹⟦ A ∧ B ; ⟦ A ; B ⟧ ⟹ C ⟧ ⟹ C›
+ apply (frule conjunct1)
+ apply (drule conjunct2)
+ apply (assumption)
+ done
+
+lemma impE: ‹⟦ P ⟶ Q; P ; Q ⟹ R ⟧ ⟹ R›
+ apply (drule mp)
+ apply assumption
+ apply assumption
+ done
+
+lemma ‹A ∧ B ⟶ B ∧ A›
+ apply (rule impI)
+ apply (erule conjE)
+ apply (rule conjI)
+ apply assumption
+ apply assumption
+ done
+
+lemma ‹X ⟶ ¬ ¬ X›
+ apply (rule impI)
+ apply (rule notI)
+ apply (erule notE)
+ apply assumption
+ done
+
+lemma ‹(X ⟶ Y ⟶ ¬ X) ⟶ X ⟶ ¬ Y›
+ apply (rule impI)
+ apply (rule impI)
+ apply (erule impE)
+ apply assumption
+ apply (rule notI)
+ apply (erule impE)
+ apply assumption
+ apply (erule notE)
+ apply assumption
+ done
+
+axiomatization where
+ classical: ‹⟦ ¬ P ⟹ P ⟧ ⟹ P›
+
+lemma ccontr: "⟦ ¬ P ⟹ False ⟧ ⟹ P"
+ apply (rule classical)
+ apply (rule FalseE)
+ by (assumption)
+
+lemma ‹¬ ¬ X ⟶ X›
+ apply (rule impI)
+ apply (rule ccontr)
+ apply (erule notE)
+ apply assumption
+ done
+
+lemma dm1: ‹¬ (A ∧ B) ⟶ ¬ A ∨ ¬ B›
+ apply (rule impI)
+ apply (rule ccontr)
+ apply (erule notE)
+ apply (rule conjI)
+ apply (rule ccontr)
+ apply (erule notE)
+ apply (rule disjI1)
+ apply assumption
+ apply (rule ccontr)
+ apply (erule notE)
+ apply (rule disjI2)
+ apply assumption
+ done
+
+lemma ‹¬ (A ⟶ B) ⟶ A›
+ apply (rule impI)
+ apply (rule ccontr)
+ apply (erule notE)
+ apply (rule impI)
+ apply (erule notE)
+ apply assumption
+ done
+
+lemma ‹¬ A ∧ ¬ B ⟶ ¬ (A ∨ B)›
+ apply (rule impI)
+ apply (erule conjE)
+ apply (rule notI)
+ apply (erule disjE)
+ apply (erule notE, assumption)
+ apply (erule notE, assumption)
+ done
+
+lemma ‹¬ (A ∨ B) ⟶ ¬ A ∧ ¬ B›
+ apply (rule impI)
+ apply (rule conjI)
+ apply (rule notI)
+ apply (erule notE)
+ apply (rule disjI1)
+ apply (assumption)
+ apply (rule notI)
+ apply (erule notE)
+ apply (rule disjI2)
+ apply (assumption)
+ done
+
+lemma ‹(A ⟶ B) ⟶ ((B ⟶ C) ⟶ A) ⟶ B›
+ apply (intro impI)
+ apply (rule ccontr)
+ apply (erule impE)
+ apply (drule mp)
+ apply (rule impI)
+ apply (erule notE)
+ apply assumption
+ apply assumption
+ apply (erule notE)
+ apply assumption
+ done
+
+axiomatization
+ All :: ‹('a ⇒ bool) ⇒ bool› (binder "∀" 10) and
+ Ex :: ‹('a ⇒ bool) ⇒ bool› (binder "∃" 10)
+where
+ allI : ‹⟦ ⋀x. P x ⟧ ⟹ ∀ x. P x› and
+ spec : ‹∀ a. P a ⟹ P x› and
+ exI : ‹⟦ P x ⟧ ⟹ ∃a. P a› and
+ exE : ‹⟦ ∃ x. P x ; ⋀a. P a ⟹ R ⟧ ⟹ R›
+
+lemma allE : ‹⟦ ∀a. P a; P x ⟹ R ⟧ ⟹ R›
+ apply (drule_tac x = x in spec)
+ apply assumption
+ done
+
+lemma ‹∀x. ¬ P x ⟹ ¬ (∃x. P x)›
+ apply (rule notI)
+ apply (erule exE)
+ apply (erule_tac x = a in allE)
+ apply (erule notE)
+ apply assumption
+ done
+
+
+lemma foobl: ‹¬ (∃x. P x) ⟹ ∀x. ¬ P x›
+ apply (intro allI notI)
+ apply (erule notE)
+ apply (rule exI)
+ apply assumption
+ done
+
+lemma ‹∃ x y. P x y ⟹ ∃ y x. P x y›
+ apply (elim exE)
+ apply (intro exI)
+ apply assumption
+ done
+
+lemma ‹∃ x. P x ⟶ Q ⟹ (∀ x. P x) ⟶ Q›
+ apply (intro impI)
+ apply (elim exE)
+ apply (drule_tac x = a in spec)
+ apply (drule mp, assumption)
+ apply assumption
+ done
+
+
+lemma ‹(∀ x. P x) ⟶ Q ⟹ ∃ x. P x ⟶ Q›
+ apply (rule ccontr)
+ apply (elim impE)
+ apply (intro allI)
+ apply (rule ccontr)
+ apply (erule notE)
+ apply (rule_tac x = x in exI)
+ apply (rule impI)
+ apply (erule notE)
+ apply assumption
+ apply (erule notE)
+ apply (intro exI)
+ apply (rule impI)
+ apply assumption
+ done
+
+lemma ‹(∀ x. P x) ⟶ (∃ x. Q x) ⟹ ∃ x. P x ⟶ Q x›
+ apply (rule ccontr)
+ apply (elim impE)
+ apply (intro allI)
+ apply (rule ccontr)
+ apply (erule notE)
+ apply (rule_tac x = x in exI)
+ apply (rule impI)
+ apply (erule notE)
+ apply assumption
+ apply (erule notE)
+ apply (erule exE)
+ apply (intro exI)
+ apply (rule impI)
+ apply assumption
+ done
+
+
+lemma ‹ ∃ x. P x ⟶ Q x ⟹ (∀ x. P x) ⟶ (∃ x. Q x)›
+ apply (rule impI)
+ apply (elim exE)
+ apply (drule_tac x = a in spec)
+ apply (drule mp, assumption)
+ apply (rule exI)
+ apply assumption
+ done
+
+lemma ‹∀ x. ¬ R x ⟶ R (M x) ⟹ ∀ x. R x ∨ R (M x)›
+ apply (intro allI)
+ apply (erule_tac x = x in allE)
+ apply (rule ccontr)
+ apply (erule impE)
+ apply (rule notI)
+ apply (erule notE)
+ apply (rule disjI1)
+ apply assumption
+ apply (erule notE)
+ apply (rule disjI2)
+ apply assumption
+ done
+
+lemma helper: "¬ A ⟶ B ⟹ A ∨ B"
+ apply (rule ccontr)
+ apply (erule impE)
+ apply (rule notI)
+ apply (erule notE)
+ apply (rule disjI1)
+ apply assumption
+ apply (erule notE)
+ apply (rule disjI2)
+ apply assumption
+ done
+
+lemma ‹⟦∀ x. ¬ R x ⟶ R (M x); ∃ x. R x ⟧ ⟹ ∃ x. R x ∧ R (M (M x))›
+ apply (erule exE)
+ apply (frule_tac x = a in allE, assumption)
+ apply (drule_tac x = a in spec)
+ apply (frule_tac x = "M a" in spec)
+ apply (drule_tac x = "M (M a)" in spec)
+ apply (drule helper)+
+ apply (elim disjE)
+ apply (rule_tac x = a in exI; intro conjI; assumption)
+ apply (rule_tac x = "M a" in exI; intro conjI; assumption)
+ apply (rule_tac x = a in exI; intro conjI; assumption)
+ apply (rule_tac x = a in exI; intro conjI; assumption)
+ apply (rule_tac x = a in exI; intro conjI; assumption)
+ apply (rule_tac x = "M a" in exI; intro conjI; assumption)
+ apply (rule_tac x = a in exI; intro conjI; assumption)
+ apply (rule_tac x = a in exI; intro conjI; assumption)
+ done
+}
\ No newline at end of file
diff --git a/trees/isa-0003.tree b/trees/isa-0003.tree
new file mode 100644
index 0000000..bda317c
--- /dev/null
+++ b/trees/isa-0003.tree
@@ -0,0 +1,6 @@
+\date{2025-11-25T14:01:00Z}
+\author{liamoc}
+\title{Isabelle and HOL}
+\[width]{250px}[class]{portrait}[style]{border:0px}[src]{\route-asset{assets/isabelle_hol.svg}}{}
+\p{These lectures introduce theorem proving using the proof assistant [Isabelle](https://isabelle.in.tum.de/). Isabelle supports many logics, but by far the most popular is \strong{H}igher \strong{O}rder \strong{L}ogic, the focus of these notes. Isabelle comes pre-packaged with its HOL libraries, as well as a proof editor (based on jEdit) and various other tools. }
+\p{The proof developments shown in these notes are all developed with Isabelle 2024, but Isabelle 2025 (the latest version at time of writing) is largely backwards compatible with it. I have not upgraded due to some proof automation regressions in Isabelle 2025 that do not affect the content of these notes.}
\ No newline at end of file
diff --git a/trees/loc-002D.tree b/trees/loc-002D.tree
index 4ef9bcf..fc66158 100644
--- a/trees/loc-002D.tree
+++ b/trees/loc-002D.tree
@@ -17,6 +17,7 @@
\li{Ash - Ash Wednesday to Easter for Choirs, Oxford.}
\li{Adv - Advent for Choirs, Oxford.}
\li{#{n}thCh - #{n}th Chester Book of Motets.}
+ \li{FaberTal - Faber Choral Programme Series, Thomas Tallis volume.}
\li{Loose - not in a volume but a separate copy.}
}
}