From 7410478870293074c1b2467c3480da9d37163d4a Mon Sep 17 00:00:00 2001 From: Liam O'Connor Date: Wed, 26 Nov 2025 01:27:01 +1100 Subject: [PATCH] starting isa --- assets/isabelle_hol.svg | 363 ++++++++++++ assets/music.tsv | 1205 ++++++++++++++++++++------------------- trees/isa-0002.tree | 295 ++++++++++ trees/isa-0003.tree | 6 + trees/loc-002D.tree | 1 + 5 files changed, 1270 insertions(+), 600 deletions(-) create mode 100644 assets/isabelle_hol.svg create mode 100644 trees/isa-0002.tree create mode 100644 trees/isa-0003.tree 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 @@ + + + + + + + image/svg+xml + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + → + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + 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.} } } -- 2.51.2