+54 -31

assets/music.tsv

reviewed

··· 9 9 Anon. Easter Alleluias: (a) Antiphon with psalm tone, (b) Plainchant Alleluia Ash p154 🟢 10 10 Anon. Come, rock the cradle for him CfC3 p53 11 11 Anon. (16th Century) O Lord, the maker of all thing XVIAB p85 12 12 - Anon. (16th Century) Rejoice in the Lord alway XVIAB p1; Adv p162 🟢 12 12 + Anon. (16th Century) Rejoice in the Lord alway XVIAB p1; Adv p162; ECM1 p1 🟢 13 13 Anon. (16th Century) This is the day XVIAB p32 14 14 Arcadelt Haec dies NCAB p146; 5thCh p2 15 15 Arcadelt O Lord, my God, to thee NCAB p293 ··· 62 62 Bain Brother James' Air NOEAB p30 63 63 Bainton A babe is born I wys CfC2 p6 64 64 Bairstow I sat down under his shadow AfC1 p74 🟢 65 65 - Bairstow Jesu, the very thought of thee NCAB p197 65 65 + Bairstow Jesu, the very thought of thee NCAB p197; ECM1 p6 66 66 Bairstow Let all mortal flesh keep silence AfC4 p88 67 67 Bairstow Psalm 114 Ash p165 68 68 Bairstow The day draws on with golden light NCAB p436 ··· 92 92 Blackwell (arr.) O Thou, whose all-redeeming might NOEAB p168 93 93 Blow Let my prayer AfC1 p86 94 94 Blow Praise the Lord, ye servants AfC1 p174 95 95 + Blow Salvator mundi ECM1 p9 🟢 95 96 Bohemian Brethren (arr. Guest) Zion, at thy shining gates Adv p214 96 97 Bourgeois O gladsome light, O grace NCAB p273 97 98 Bourgeois O strength and stay AfC1 p156 98 99 Bourne Thou art God NOEAB p231 100 100 + Boyce O where shall wisdom be found? ECM1 p16 99 101 Brahms Ah, thou poor world AfC1 p10 100 102 Britten A boy was born CfC1 p4 101 103 Britten A new year carol CfC2 p64 ··· 113 115 Bullock Give us the wings of faith AfC4 p128 114 116 Bullock Good Christian men rejoice and sing OEAB p38 115 117 Bullock (arr.) Give laud unto the Lord OEAB p64 116 116 - Byrd Ave verum corpus NCAB p38; OBTA p44; 2ndCh p2 🟢 118 118 + Byrd Ave verum corpus NCAB p38; OBTA p44; 2ndCh p2; ECM1 p32 🟢 117 119 Byrd Cibavit eos 2ndCh p6 118 120 Byrd Civitas sancti tui Ash p4 🟢 119 119 - Byrd Haec dies OBTA p84 🟢 120 120 - Byrd Justorum animae OBTA p131 121 121 + Byrd Haec dies OBTA p84; ECM1 p36 🟢 122 122 + Byrd Justorum animae OBTA p131; ECM1 p42 121 123 Byrd Laetentur coeli OBTA p137 122 124 Byrd Mass for five voices Loose. Chester edition 🟢 123 125 Byrd Miserere mei OBTA p157 124 126 Byrd O quam gloriosum OBTA p256 125 127 Byrd Sacerdotes Domini NCAB p399; XVIAB p55 126 128 Byrd Senex puerum 2ndCh p10 127 127 - Byrd Sing joyfully OBTA p287 🟢 129 129 + Byrd Sing joyfully OBTA p287; ECM1 46 🟢 128 130 Byrd Teach me, O Lord OBTA p298 129 131 Byrd This day Christ was born OBTA p307 130 132 Byrd Venite comedite 2ndCh p13 ··· 174 176 Elgar Ave verum corpus NCAB p44 🟢 175 177 Elgar Dream of Gerontius Loose. 1900 Novello edition 176 178 Elgar Light of the World Ash p170 177 177 - Elgar O salutaris Hostia No. 3 NOEAB p157 179 179 + Elgar O salutaris Hostia NOEAB p157 180 180 + Elgar They are at rest ECM1 p53 178 181 Ellis There is no rose NOEAB p221 🟢 179 182 Esquivel Ego sum panis vivus 3rdCh p2 180 183 Este's Psalter While shepherds watched their flocks by night CfC1 p166 (arr. Ravenscroft), CfC2 p210 (arr. Willcocks) 🟢 181 184 Farrant Call to remembrance NCAB p87; OBTA p50 🟢 182 185 Farrant Hide not thou thy face NCAB p151; OBTA p94 🟢 183 183 - Farrant (attrib.) Lord, for thy tender mercy's sake NOEAB p138; NCAB p224; OBTA p152; Ash p13 🟢 186 186 + Farrant (attrib.) Lord, for thy tender mercy's sake NOEAB p138; NCAB p224; OBTA p152; Ash p13; ECM1 p76 🟢 184 187 Farrar Almighty God, the fountain of all wisdom AfC1 p24 185 188 Ferguson (arr.) People look East Adv p157 186 189 Ford Almighty God, which hast me brought NCAB p21; AfC1 p28 ··· 191 194 Gibbons Almighty and everlasting God NCAB p18; OBTA p15 🟢 192 195 Gibbons Drop, drop, slow tears NOEAB p52; NCAB p116 🟢 193 196 Gibbons Hosanna to the Son of David OBTA p99 194 194 - Gibbons O clap your hands OBTA p164 195 195 - Gibbons O Lord, in thy wrath OBTA p231 197 197 + Gibbons O clap your hands OBTA p164; ECM1 p53 198 198 + Gibbons O Lord, in thy wrath OBTA p231; ECM1 p57 196 199 Gibbons Song 44 AfC1 p46 197 200 Gibbons Song 46 AfC1 p30 198 201 Gibbons This is the record of John NCAB p454; OBTA p318 🟢 ··· 203 206 Goss O pray for the peace of Jerusalem AfC1 p146 204 207 Goss O Saviour of the world NCAB p323; NOEAB p163 🟢 205 208 Goss See amid the winter's snow CfC1 p103 206 206 - Goss These are they which follow the Lamb AfC1 p200 209 209 + Goss These are they which follow the Lamb AfC1 p200; ECM1 p78 207 210 Greene Thou visitest the earth NCAB p473 🟢 211 211 + Greene Lord, let me know mine end ECM1 p80 208 212 Gritton Lord that descendedst, Holy Child AfC1 p98 209 213 Gruber Stille Nacht CfC2 p184 (arr. Willcocks), CfC3 p168 (arr. Cashmore) 🟢 210 214 Guerrero Canite tuba Adv p49; 3rdCh p5 211 215 Guerrero Gloriose confessor 3rdCh p9 212 216 Hadley I sing of a maiden CfC2 p86 217 217 + Hadley My song is love unknown ECM1 p90 213 218 Halls Hosanna to the Son of David NOEAB p88 214 219 Halls Wash me throughly NOEAB p244 215 220 Händel Ecce quomodo moritur justus Ash p67 ··· 221 226 Hare Thou, O God, art praised in Sion AfC4 p94 222 227 Harris Behold, the tabernacle of God NCAB p58 223 228 Harris Come down, O Love divine NCAB p94 224 224 - Harris Faire is the heaven AfC4 p100 229 229 + Harris Faire is the heaven AfC4 p100; ECM1 p96 225 230 Harris Fear not, O land NOEAB p57 226 231 Harris Holy is the true light NCAB p164 227 232 Harris Most glorious Lord of life OEAB p163; Ash p182 228 233 Harris Vexilla Regis Cunctis (Tarry no longer; toward thine heritage) OEAB p167 229 234 Harris (arr.) O strength and stay AfC1 p156 235 235 + Harwood O how glorious is the kingdom ECM1 p115 230 236 Hassler Cantate Domino 4thCh p18 🟢 231 237 Hassler Laetentur caeli 4thCh p21 232 238 Hassler Tu es Petrus 4thCh p24 ··· 239 245 How Advent Message NOEAB p2 240 246 How Day by day NOEAB p49 🟢 241 247 How Praise, O praise NCAB p359 242 242 - Howells Like as the hart AfC4 p158 🟢 248 248 + Howells Like as the hart AfC4 p158; ECM1 p126 🟢 243 249 Howells My eyes for beauty pine NCAB p235; NOEAB p152; OEAB p169 🟢 244 250 Howells Tryste noel CfC3 p172 245 251 Hurford Litany to the Holy Spirit NOEAB p133 246 252 Hurford Sunny bank CfC3 p36 247 253 Hutchings Hosanna to the Son of David Ash p84 248 254 Ingegneri In monte oliveti 1stCh p10 249 249 - Ireland Greater love hath no man AfC4 p174 🟢 255 255 + Ireland Greater love hath no man AfC4 p174; ECM1 p132 🟢 250 256 Isaac Gustate et videte 5thCh p9 251 257 Isaac Ierusalem surge 5thCh p11 252 258 Isom King of all ages, throned on high NOEAB p123 🟢 ··· 289 295 Ley Lo, round the throne a glorious band NCAB p215 🟢 290 296 Ley The strife is o'er NCAB p448 291 297 Ley (arr.) A Choral Hymn for Advent or Ascensiontide) OEAB p68 298 298 + Lewis The souls of the righteous ECM1 p141 292 299 Lindley (arr.) Now the green blade riseth Ash p190 293 300 Lloyd Drop down, ye heavens Adv p61 294 301 Lole Jesu, the very thought of thee NOEAB p108 ··· 311 318 McKie We wait for thy loving kindness AfC4 p77 🟢 312 319 Mendelssohn Above all praise NCAB p10; OEAB p74 313 320 Mendelssohn Hark! the herald angels sing CfC1 p39 (with Willcocks descant), CfC3 p68 🟢 321 321 + Mendelssohn Hear my prayer ECM1 p146 314 322 Mendelssohn How lovely are the messengers (from Saint Paul) Adv p92 315 323 Mendelssohn Sleepers, wake AfC1 p192 316 324 Mendelssohn When Jesus, our Lord NCAB p512 ··· 323 331 Morgan A Palm Sunday Antiphon NCAB p5 324 332 Morley Agnus Dei Ash p33; 2ndCh p20 325 333 Morley Eheu, sustulerunt Ash p139 326 326 - Morley Nolo mortem peccatoris NCAB p259; XVIAB p13 🟢 334 334 + Morley Nolo mortem peccatoris NCAB p259; XVIAB p13; ECM p162 🟢 327 335 Mozart Ave verum corpus NCAB p48; NOEAB p14; OEAB p29 🟢 328 336 Mozart Grosse Messe Loose; Breitkopf edition 329 337 Mudd Let thy merciful ears, O Lord NCAB p209; OBTA p147 330 338 Mundy O Lord, the maker of all things NCAB p302; OBTA p240 331 339 Near There is no rose Adv p184 🟢 340 340 + Naylor Vox dicentis: Clama ECM1 p166 332 341 Nicolai (arr. Bach, J.S.) Wachet auf! Adv p211 🟢 333 342 Oldroyd (arr.) Ye watchers and ye holy ones OEAB p84 334 343 Ord Adam lay ybounden CfC2 p10 🟢 ··· 346 355 Palestrina Matin Responsory Adv p130; CfC2 p68 🟢 347 356 Palestrina Missa Brevis Loose. Chester edition 🟢 348 357 Palestrina O Bone Iesu (4v) OEAB p104 🟢 349 349 - Palestrina Salvator mundi NCAB p401 358 358 + Palestrina Salvator mundi NCAB p401 🟢 350 359 Palestrina Sanctus (from Missa Quarta) XVIAB p51 351 360 Palestrina Sicut cervus 1stCh p27 🟢 352 361 Palestrina Super flumina 1stCh p31 🟢 353 362 Palestrina Vesper Responsory Adv p203 🟢 354 363 Parry My soul, there is a country NCAB p244 🟢 355 364 Parry I was glad when they said unto me Loose. Novello edition 🟢 356 356 - Parsons Ave Maria OBTA p32 🟢 357 357 - Pärt Bogoroditsye Dyevo Adv p46 365 365 + Parsons Ave Maria OBTA p32; ECM1 p181 🟢 366 366 + Pärt Bogoroditsye Dyevo Adv p46 🟢 358 367 Pearsall Ave verum corpus NOEAB p18 359 368 Pearsall In dulci jubilo CfC1 p42 🟢 360 369 Peeters Ave verum corpus Ash p110 361 370 Pettman (arr.) I saw a maiden CfC2 p83 362 362 - Philips Ascendit Deus OBTA p22 🟢 371 371 + Philips Ascendit Deus OBTA p22; ECM1 p187 🟢 363 372 Philips Surgens Jesus NCAB p431 364 373 Piæ Cantiones (arr. Jaques) Good King Wenceslas CfC1 p34 365 374 Piæ Cantiones (arr. Willcocks) Of the Father's heart begotten CfC2 p128 ··· 375 384 Praetorius Puer natus est nobis 4thCh p28 376 385 Praetorius Salve rex noster 4thCh p29 377 386 Psalmodia Sacra (arr. Willcocks) Bethlehem, of noblest cities CfC3 p40 387 387 + Purcell Hear my prayer, O Lord ECM1 p193 388 388 + Purcell I was glad when they said unto me ECM1 p199 389 389 + Purcell Let mine eyes run down with tears ECM1 p210 390 390 + Purcell Lord, how long wilt thou be angry? ECM1 p224 378 391 Purcell O God the King of glory AfC1 p136 379 392 Purcell Rejoice in the Lord alway NCAB p381 393 393 + Purcell Remember not, Lord, our offences ECM1 p232 380 394 Purcell Thou knowest, Lord NCAB p463; NOEAB p236 🟢 381 395 Purcell, D. I will thank thee, O Lord NOEAB p96 382 396 Rachmaninoff To thee, O Lord AfC1 p203 ··· 443 457 Shepherd In manus tuas 2ndCh p22 444 458 Somervell O Saviour of the world NCAB p330 445 459 Soriano Regina caeli 1stCh p35 446 446 - Stainer God so loved the world NOEAB p81; Ash p72 🟢 460 460 + Stainer God so loved the world NOEAB p81; Ash p72; ECM1 p236 🟢 447 461 Stainer How beautiful upon the mountains Adv p87 462 462 + Stainer I saw the Lord ECM1 p238 463 463 + Stanford Beati quorum via ECM1 p255 🟢 448 464 Stanford Benedictus in C Adv p38 465 465 + Stanford Caelos ascendit hodie ECM1 p260 449 466 Stanford Glorious and Powerful God NCAB p129 467 467 + Stanford How beautious are their feet ECM1 p269 468 468 + Stanford I heard a voice from heaven ECM1 p276 469 469 + Stanford Justorum animae ECM1 p281 450 470 Stanford Pray that Jerusalem NCAB p372 451 471 Stanford Ye choirs of new Jerusalem AfC1 p215; Ash p216 🟢 452 472 Stanford (arr.) O for a closer walk AfC1 p142 ··· 466 486 Tallis Discomfit them, O Lord FaberTal p24 467 487 Tallis Euge caeli 2ndCh p25 468 488 Tallis I call and cry to thee, O Lord FaberTal p13 469 469 - Tallis If ye love me NCAB p177; NOEAB p98; OBTA p122; FaberTal p4 🟢 470 470 - Tallis O Lord, give thy Holy Spirit XVIAB p47; FaberTal p11 🟢 471 471 - Tallis O nata lux OBTA p248 🟢 489 489 + Tallis If ye love me NCAB p177; NOEAB p98; OBTA p122; FaberTal p4; ECM1 p298 🟢 490 490 + Tallis Loquebantur variis linguis ECM1 p285 491 491 + Tallis O Lord, give thy Holy Spirit XVIAB p47; FaberTal p11; ECM1 p293 🟢 492 492 + Tallis O nata lux OBTA p248; ECM1 p296 🟢 472 493 Tallis Hear the voice and prayer FaberTal p6 🟢 473 494 Tallis Salvator mundi OBTA p273 🟢 474 495 Tallis Sancte Deus 2ndCh p27 ··· 479 500 Tate Carol, with lullaby CfC1 p72 480 501 Taverner Alleluia 2ndCh p33 481 502 Taverner Audivi 2ndCh p35 503 503 + Taverner Dum transisset Sabbatum ECM1 p300 482 504 Tchaikovsky Holy, Holy, Holy (Hymn to the Trinity) NCAB p155 483 505 Tchaikovsky The crown of roses CfC3 p196 484 506 Terry Myn lyking CfC2 p84 ··· 488 510 Tomblings All from the sun's uprise OEAB p129 489 511 Tomkins I heard a voice OBTA p126 490 512 Tomkins O pray for the peace of Jerusalem XVIAB p101 491 491 - Tomkins When David heard OBTA p332 513 513 + Tomkins When David heard OBTA p332; ECM p307 492 514 Trevor (arr.) The angels and the shepherds CfC2 p182 493 515 Turner O Trinity, most blessed light AfC1 p159 494 516 Tye A sound of angels AfC1 p1 ··· 503 525 Vaughan Williams Let us now praise famous men NCAB p212; NOEAB p130 504 526 Vaughan Williams No sad thought his soul affright CfC1 p84 505 527 Vaughan Williams O clap your hands AfC4 p197 506 506 - Vaughan Williams O how amiable NCAB p278; OEAB p181; AfC4 p152 🟢 528 528 + Vaughan Williams O how amiable NCAB p278; OEAB p181; AfC4 p152; ECM1 p314 🟢 507 529 Vaughan Williams O little town of Bethlehem CfC1 p92 🟢 508 508 - Vaughan Williams O taste and see NOEAB p166; OEAB p106; AfC4 p86 🟢 530 530 + Vaughan Williams O taste and see NOEAB p166; OEAB p106; AfC4 p86; ECM1 p318 🟢 509 531 Vaughan Williams The Blessed son of God CfC1 p112 510 532 Vaughan Williams (arr.) All in the morning CfC3 p122 511 533 Vaughan Williams (arr.) Gloucestershire wassail CfC1 p160 🟢 ··· 535 557 Walton All this time CfC2 p13 536 558 Walton Drop, drop, slow tears Ash p41 537 559 Walton King Herod and the cock CfC3 p186 538 538 - Walton Set me as a seal AfC4 p82 560 560 + Walton Set me as a seal AfC4 p82; ECM1 p320 539 561 Walton What cheer? CfC1 p162 540 562 Warrell (arr.) A merry Christmas CfC1 p60 541 563 Waters I sing of a Maiden that is mateless OEAB p21 🟢 ··· 545 567 Weelkes Hosanna to the Son of David OBTA p113 🟢 546 568 Weelkes O Lord, arise OBTA p209 547 569 Weelkes When David heard OBTA p343 🟢 548 548 - Wesley, S. S. Blessed be the God and Father NCAB p64 🟢 570 570 + Wesley, S. S. Blessed be the God and Father NCAB p64; ECM1 p324 🟢 549 571 Wesley, S. S. Lead me, Lord NCAB p206; NOEAB p127; AfC1 p78 🟢 550 572 Wesley, S. S. O Lord my God NCAB p288 573 573 + Wesley, S. S. Praise the Lord, O my soul ECM1 p333 551 574 Wesley, S. S. Thou judge of quick and dead NCAB p458 552 552 - Wesley, S. S. Thou wilt keep him in perfect peace NCAB p482 🟢 553 553 - Wesley, S. S. Wash me throughly NCAB p502; Ash p45 575 575 + Wesley, S. S. Thou wilt keep him in perfect peace NCAB p482; ECM1 p351 🟢 576 576 + Wesley, S. S. Wash me throughly NCAB p502; Ash p45; ECM1 p356 554 577 White A Prayer of St. Richard of Chichester OEAB p177 555 578 Whitlock He is risen Ash p229 556 579 Whyte O Christ, who art the light and day AfC1 p118 ··· 593 616 Willcocks (arr.) What child is this? CfC3 p187 594 617 Wise Blessed is he that considereth NCAB p77 595 618 Wood Never weather-beaten sail NCAB p253 596 596 - Wood O thou, the central orb NCAB p340; AfC4 p9; Adv p149 🟢 619 619 + Wood O thou, the central orb NCAB p340; AfC4 p9; Adv p149; ECM1 p361 🟢 597 620 Wood Oculi omnium NCAB p349 598 621 Wood (arr.) A virgin most pure CfC1 p14 599 622 Wood (arr.) God rest you merry, gentlemen CfC1 p29

+11 -59

trees/isa-0002.tree

reviewed

··· 1 1 \date{2025-11-25} 2 2 \author{liamoc} 3 3 - \title{Natural Deduction} 3 3 + \title{Building up HOL} 4 4 \taxon{Lecture} 5 5 \import{shiki-macros} 6 6 \put\shiki/language{Isabelle Theory} ··· 15 15 judgment Trueprop :: "bool ⇒ prop" (‹(_)› 5) 16 16 } 17 17 18 18 + \transclude{isa-0005} 19 19 + \transclude{isa-0004} 20 20 + \transclude{isa-0006} 21 21 + \transclude{isa-0007} 22 22 + \transclude{isa-0008} 18 23 19 24 20 20 - \shiki{axiomatization 21 21 - conj :: "bool ⇒ bool ⇒ bool" (infixr "∧" 35) and 22 22 - where 23 23 - (* Conjunction *) 24 24 - conjI : "⟦ A ; B ⟧ ⟹ (A ∧ B)" and 25 25 - conjunct1 : "A ∧ B ⟹ A" and 26 26 - conjunct2 : "A ∧ B ⟹ B" 27 27 - } 28 28 - 29 25 \shiki{ 30 30 - disj :: "bool ⇒ bool ⇒ bool" (infixr "∨" 30) and 31 31 - implies :: "bool ⇒ bool ⇒ bool" (infixr "⟶" 25) and 32 32 - not :: "bool ⇒ bool" ("¬ _" [40] 40) 33 33 - 34 34 - (* Disjunction *) 35 35 - disjI1 : "A ⟹ (A ∨ B)" and 36 36 - disjI2 : "B ⟹ (A ∨ B)" and 37 37 - disjE : "⟦ A ∨ B ; A ⟹ C ; B ⟹ C ⟧ ⟹ C" and 38 38 - 39 39 - (* Implication *) 40 40 - impI : "(A ⟹ B) ⟹ (A ⟶ B)" and 41 41 - mp : "⟦ A ⟶ B ; A ⟧ ⟹ B" and 42 42 - 43 43 - (* Negation *) 44 44 - notI : "(A ⟹ False) ⟹ ¬ A" and 45 45 - notE : "⟦ ¬ A ; A ⟧ ⟹ R" and 46 46 - 47 47 - (* False and True *) 48 48 - FalseE : "False ⟹ C" and 49 49 - TrueI : "True" 50 50 - 51 26 lemma conjE : ‹⟦ A ∧ B ; ⟦ A ; B ⟧ ⟹ C ⟧ ⟹ C› 52 27 apply (frule conjunct1) 53 28 apply (drule conjunct2) ··· 58 33 apply (drule mp) 59 34 apply assumption 60 35 apply assumption 61 61 - done 62 62 - 63 63 - lemma ‹A ∧ B ⟶ B ∧ A› 64 64 - apply (rule impI) 65 65 - apply (erule conjE) 66 66 - apply (rule conjI) 67 67 - apply assumption 68 68 - apply assumption 69 69 - done 36 36 + done} 70 37 71 71 - lemma ‹X ⟶ ¬ ¬ X› 72 72 - apply (rule impI) 73 73 - apply (rule notI) 74 74 - apply (erule notE) 75 75 - apply assumption 76 76 - done 77 77 - 78 78 - lemma ‹(X ⟶ Y ⟶ ¬ X) ⟶ X ⟶ ¬ Y› 79 79 - apply (rule impI) 80 80 - apply (rule impI) 81 81 - apply (erule impE) 82 82 - apply assumption 83 83 - apply (rule notI) 84 84 - apply (erule impE) 85 85 - apply assumption 86 86 - apply (erule notE) 87 87 - apply assumption 88 88 - done 89 89 - 38 38 + \transclude{isa-0009} 39 39 + \transclude{isa-000A} 40 40 + \transclude{isa-000B} 41 41 + \shiki{ 90 42 axiomatization where 91 43 classical: ‹⟦ ¬ P ⟹ P ⟧ ⟹ P› 92 44

+19

trees/isa-0004.tree

reviewed

··· 1 1 + \date{2025-11-25T20:14:40Z} 2 2 + \author{liamoc} 3 3 + \title{Disjunction} 4 4 + \taxon{Definition} 5 5 + \parent{isa-0002} 6 6 + \import{shiki-macros} 7 7 + \put\shiki/language{Isabelle Theory} 8 8 + 9 9 + ##{\dfrac{A}{A \lor B}\text{\small disjI1}\quad 10 10 + \dfrac{B}{A \lor B}\text{\small disjI2}\quad 11 11 + \dfrac{\begin{array}{lcc}&A & B\\ & \vdots & \vdots \\A \lor B & C & C\end{array}}{C}\text{\small disjE} } 12 12 + 13 13 + \shiki{axiomatization 14 14 + disj :: "bool ⇒ bool ⇒ bool" (infixr "∨" 30) 15 15 + where 16 16 + disjI1 : "A ⟹ (A ∨ B)" and 17 17 + disjI2 : "B ⟹ (A ∨ B)" and 18 18 + disjE : "⟦ A ∨ B ; A ⟹ C ; B ⟹ C ⟧ ⟹ C" 19 19 + }

+19

trees/isa-0005.tree

reviewed

··· 1 1 + \date{2025-11-25T20:14:40Z} 2 2 + \author{liamoc} 3 3 + \title{Conjunction} 4 4 + \taxon{Definition} 5 5 + \parent{isa-0002} 6 6 + \import{shiki-macros} 7 7 + \put\shiki/language{Isabelle Theory} 8 8 + 9 9 + ##{\dfrac{A\quad B}{A \land B}\text{\small conjI}\quad 10 10 + \dfrac{A\land B}{A}\text{\small conjunct1}\quad 11 11 + \dfrac{A\land B}{B}\text{\small conjunct2} } 12 12 + 13 13 + \shiki{axiomatization 14 14 + conj :: "bool ⇒ bool ⇒ bool" (infixr "∧" 35) 15 15 + where 16 16 + conjI : "⟦ A ; B ⟧ ⟹ (A ∧ B)" and 17 17 + conjunct1 : "A ∧ B ⟹ A" and 18 18 + conjunct2 : "A ∧ B ⟹ B" 19 19 + }

+20

trees/isa-0006.tree

reviewed

··· 1 1 + \date{2025-11-25T20:14:40Z} 2 2 + \author{liamoc} 3 3 + \title{Implication} 4 4 + \taxon{Definition} 5 5 + \parent{isa-0002} 6 6 + \import{shiki-macros} 7 7 + \put\shiki/language{Isabelle Theory} 8 8 + 9 9 + ##{ 10 10 + \dfrac{\begin{array}{c}A\\ \vdots \\ B \end{array}}{A \rightarrow B}\text{\small impI} \quad 11 11 + \dfrac{A \rightarrow B \quad A}{B}\text{\small mp} 12 12 + } 13 13 + 14 14 + 15 15 + \shiki{axiomatization 16 16 + implies :: "bool ⇒ bool ⇒ bool" (infixr "⟶" 25) 17 17 + where 18 18 + impI : "(A ⟹ B) ⟹ (A ⟶ B)" and 19 19 + mp : "⟦ A ⟶ B ; A ⟧ ⟹ B" 20 20 + }

+21

trees/isa-0007.tree

reviewed

··· 1 1 + \date{2025-11-25T20:14:40Z} 2 2 + \author{liamoc} 3 3 + \title{False and True} 4 4 + \taxon{Definition} 5 5 + \parent{isa-0002} 6 6 + \import{shiki-macros} 7 7 + \put\shiki/language{Isabelle Theory} 8 8 + 9 9 + ##{ 10 10 + \dfrac{\quad}{\textsf{True}}\text{\small TrueI} \quad 11 11 + \dfrac{\textsf{False}}{P}\text{\small FalseE} 12 12 + } 13 13 + 14 14 + 15 15 + \shiki{axiomatization 16 16 + False :: "bool" and 17 17 + True :: "bool" 18 18 + where 19 19 + FalseE : "False ⟹ C" and 20 20 + TrueI : "True" 21 21 + }

+20

trees/isa-0008.tree

reviewed

··· 1 1 + \date{2025-11-25T20:14:40Z} 2 2 + \author{liamoc} 3 3 + \title{Negation} 4 4 + \taxon{Definition} 5 5 + \parent{isa-0002} 6 6 + \import{shiki-macros} 7 7 + \put\shiki/language{Isabelle Theory} 8 8 + 9 9 + ##{ 10 10 + \dfrac{\begin{array}{c} A \\ \vdots \\ \textsf{False}\end{array}}{\neg A}\text{\small notI} \quad 11 11 + \dfrac{\neg A\quad A}{R}\text{\small notE} 12 12 + } 13 13 + 14 14 + 15 15 + \shiki{axiomatization 16 16 + not :: "bool ⇒ bool" ("¬ _" [40] 40) 17 17 + where 18 18 + notI : "(A ⟹ False) ⟹ ¬ A" and 19 19 + notE : "⟦ ¬ A ; A ⟧ ⟹ R" 20 20 + }

+16

trees/isa-0009.tree

reviewed

··· 1 1 + \date{2025-11-25T20:51:35Z} 2 2 + \taxon{Example} 3 3 + \author{liamoc} 4 4 + \import{shiki-macros} 5 5 + \parent{isa-0002} 6 6 + \import{dt-macros} 7 7 + \put\shiki/language{Isabelle Theory} 8 8 + 9 9 + \shiki{lemma ‹A ∧ B ⟶ B ∧ A›} 10 10 + 11 11 + \solnblock{\shiki{apply (rule impI) 12 12 + apply (erule conjE) 13 13 + apply (rule conjI) 14 14 + apply assumption 15 15 + apply assumption 16 16 + done}}

+15

trees/isa-000A.tree

reviewed

··· 1 1 + \date{2025-11-25T20:51:35Z} 2 2 + \taxon{Example} 3 3 + \author{liamoc} 4 4 + \import{shiki-macros} 5 5 + \import{dt-macros} 6 6 + \put\shiki/language{Isabelle Theory} 7 7 + \parent{isa-0002} 8 8 + 9 9 + \shiki{lemma ‹X ⟶ ¬ ¬ X›} 10 10 + 11 11 + \solnblock{\shiki{apply (rule impI) 12 12 + apply (rule notI) 13 13 + apply (erule notE) 14 14 + apply assumption 15 15 + done}}

+20

trees/isa-000B.tree

reviewed

··· 1 1 + \date{2025-11-25T20:57:52Z} 2 2 + \taxon{Exercise} 3 3 + \author{liamoc} 4 4 + \import{shiki-macros} 5 5 + \import{dt-macros} 6 6 + \put\shiki/language{Isabelle Theory} 7 7 + \parent{isa-0002} 8 8 + 9 9 + \shiki{lemma ‹(X ⟶ Y ⟶ ¬ X) ⟶ X ⟶ ¬ Y›} 10 10 + 11 11 + \solnblock{\shiki{apply (rule impI) 12 12 + apply (rule impI) 13 13 + apply (erule impE) 14 14 + apply assumption 15 15 + apply (rule notI) 16 16 + apply (erule impE) 17 17 + apply assumption 18 18 + apply (erule notE) 19 19 + apply assumption 20 20 + done}}

+29 -3

trees/loc-002D.tree

reviewed

··· 18 18 \li{Adv - Advent for Choirs, Oxford.} 19 19 \li{#{n}thCh - #{n}th Chester Book of Motets.} 20 20 \li{FaberTal - Faber Choral Programme Series, Thomas Tallis volume.} 21 21 + \li{ECM#{n} - English Church Music, Volume #{n}, Oxford Choral Classics.} 21 22 \li{Loose - not in a volume but a separate copy.} 22 23 } 23 24 } 24 24 - 25 25 - 26 26 - \tsvtable{\route-asset{assets/music.tsv}} 25 25 + \tsvtable{\route-asset{assets/music.tsv}} 26 26 + \subtree{ 27 27 + \title{Chant Books} 28 28 + \ul{ 29 29 + \li{\strong{Office} 30 30 + \ul{ 31 31 + \li{\em{Anglican}: A Manual of Plainsong, RSCM Chant Book, The Cathedral Psalter, The Parish Psalter with Chants, The Australian Psalter, Sarum Compline (BCP English)} 32 32 + \li{\em{Latin}: Sarum Matins (IA-IIIC, Latin), Sarum Diurnal (I-III, Latin), Sarum Vespers (I-III, Latin), Sarum Compline (Latin), Les Heures Gregoriennes (I-III), Psalterium Romanum, Antiphonale Ambrosianum (I-IV), Roman Compline, Antiphonale Romanum (I-II, Solesmes), Antiphonale Monasticum (I-III, Solesmes), Liber Hymnarius (Solesmes), Monastic Diurnal.} 33 33 + }} 34 34 + \li{\strong{Mass} 35 35 + \ul{ 36 36 + \li{\em{Anglican}: Common Praier Noted (Marbeck, 1550), Plainchant Gradual (I-IV), The American Gradual 2020, The Anglican Use Gradual (2nd Edition). } 37 37 + \li{\em{Latin}: Graduale Triplex (Solesmes), Gregorian Missal (Solesmes), Offertoriale Triplex (Solesmes), Liber Cantualis (Solesmes), Liber Usualis (Solesmes, 1952), Graduale Simplex (Solesmes), Graduale Romanum Organ Accompaniments (I-IV, Solesmes), Graduale Novum (I-II)} 38 38 + }} 39 39 + } 40 40 + } 41 41 + \subtree{ 42 42 + \title{Hymnals} 43 43 + \ul{\li{The Book of Common Praise with Australian Supplement (Full Music Edition).} 44 44 + \li{The St. Gregory Hymnal and Catholic Choir Book.} 45 45 + \li{The New English Hymnal (Full Music Edition)} 46 46 + \li{New English Praise (Full Music Edition)} 47 47 + \li{Ancient and Modern (Full Music Edition)} 48 48 + \li{The Australian Hymn Book} 49 49 + \li{Together in Song (Harmony Edition)} 50 50 + \li{가톨릭 성가} 51 51 + \li{The Oxford Book of Carols}} 52 52 + }