> 1700786436 825655 PRIVMSG #esolangs :14[[07Parrot14]]4 M10 02https://esolangs.org/w/index.php?diff=119816&oldid=117877 5* 03CreeperBomb 5* (+18) 10
< 1700792081 752910 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca QUIT :Ping timeout: 256 seconds
< 1700796286 924978 :ais523!~ais523@user/ais523 QUIT :Ping timeout: 255 seconds
< 1700796691 861091 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name)
< 1700801714 10176 :zzo38!~zzo38@host-24-207-52-143.public.eastlink.ca JOIN #esolangs zzo38 :zzo38
< 1700803727 163974 :Sgeo!~Sgeo@user/sgeo QUIT :Read error: Connection reset by peer
< 1700807173 504778 :Sgeo!~Sgeo@user/sgeo JOIN #esolangs Sgeo :realname
< 1700809099 998450 :ais523!~ais523@user/ais523 QUIT :Quit: quit
> 1700810301 716229 PRIVMSG #esolangs :14[[07Special:Log/move14]]4 move_redir10 02 5* 03PythonshellDebugwindow 5*  10moved [[02Language of Lauging10]] to [[Language of Laughing]] over redirect: Fix typo
> 1700810301 741633 PRIVMSG #esolangs :14[[07Special:Log/delete14]]4 delete_redir10 02 5* 03PythonshellDebugwindow 5*  10PythonshellDebugwindow deleted redirect [[02Language of Laughing10]] by overwriting: Deleted to make way for move from "[[Language of Lauging]]"
> 1700810435 303282 PRIVMSG #esolangs :14[[07Language of Laughing14]]4 M10 02https://esolangs.org/w/index.php?diff=119819&oldid=119817 5* 03PythonshellDebugwindow 5* (+22) 10Category
< 1700811100 179232 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User
< 1700815325 793405 :cpressey!~cpressey@host-89-240-119-39.as13285.net JOIN #esolangs cpressey :[https://web.libera.chat] cpressey
< 1700815882 742957 :cpressey!~cpressey@host-89-240-119-39.as13285.net QUIT :Ping timeout: 250 seconds
< 1700816125 779314 :Koen!~Koen@2a01:e34:ec7c:30:213f:77ef:d1ad:760e JOIN #esolangs * :Koen
< 1700818010 815946 :cpressey!~cpressey@host-89-240-119-39.as13285.net JOIN #esolangs cpressey :[https://web.libera.chat] cpressey
< 1700818498 374065 :__monty__!~toonn@user/toonn JOIN #esolangs toonn :Unknown
> 1700820232 527095 PRIVMSG #esolangs :14[[07Unmatched (14]]4 10 02https://esolangs.org/w/index.php?diff=119820&oldid=119429 5* 03None1 5* (+27) 10/* Python interpreter */  Belongs to the stupid family because of its stupid error reporting feature
< 1700820518 171133 :cpressey!~cpressey@host-89-240-119-39.as13285.net PRIVMSG #esolangs :"Forward and backward proof in HOL corresponds to special cases of rule composition in Isabelle. However, Milner’s key idea of using ML’s abstract types to ensure that theorems can only be obtained by allowable combinations of allowable rules is retained, and lifted to the metalogic level."
< 1700820541 567690 :Lord_of_Life!~Lord@user/lord-of-life/x-2819915 QUIT :Ping timeout: 276 seconds
< 1700820551 260247 :cpressey!~cpressey@host-89-240-119-39.as13285.net PRIVMSG #esolangs :OK, now I'm going to have to look into Isabelle's innards to find out what the heck *that* means.
< 1700820565 966951 :Lord_of_Life!~Lord@user/lord-of-life/x-2819915 JOIN #esolangs Lord_of_Life :Lord
< 1700821783 986200 :cpressey!~cpressey@host-89-240-119-39.as13285.net PRIVMSG #esolangs :Apparently it means the metalogic is implemented as an abstract data type in ML.  The object logic that you actually work with, e.g. Isabelle/HOL, is encoded in the metalogic.
< 1700821879 352229 :cpressey!~cpressey@host-89-240-119-39.as13285.net PRIVMSG #esolangs :That seems less cool somehow. Ah well
< 1700823871 946400 :Sgeo!~Sgeo@user/sgeo QUIT :Read error: Connection reset by peer
< 1700826179 130271 :cpressey!~cpressey@host-89-240-119-39.as13285.net QUIT :Quit: Client closed
< 1700826367 787812 :cpressey!~cpressey@host-89-240-119-39.as13285.net JOIN #esolangs cpressey :[https://web.libera.chat] cpressey
< 1700827301 943534 :Koen!~Koen@2a01:e34:ec7c:30:213f:77ef:d1ad:760e QUIT :Remote host closed the connection
< 1700828022 293954 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
< 1700828047 88031 :cpressey!~cpressey@host-89-240-119-39.as13285.net QUIT :Quit: Client closed
< 1700828216 812188 :cpressey!~cpressey@host-89-240-119-39.as13285.net JOIN #esolangs cpressey :[https://web.libera.chat] cpressey
< 1700828387 122077 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User
< 1700831481 68048 :Koen!~Koen@78.199.192.3 JOIN #esolangs * :Koen
< 1700834446 755805 :cpressey!~cpressey@host-89-240-119-39.as13285.net QUIT :Ping timeout: 250 seconds
< 1700835024 678325 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
< 1700835060 830588 :cpressey!~cpressey@host-89-240-119-39.as13285.net JOIN #esolangs cpressey :[https://web.libera.chat] cpressey
< 1700835382 28591 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User
> 1700837286 71684 PRIVMSG #esolangs :14[[07Wiwa14]]4 10 02https://esolangs.org/w/index.php?diff=119821&oldid=119811 5* 030ptr 5* (+56) 10
> 1700840236 795766 PRIVMSG #esolangs :14[[07Kak14]]4 10 02https://esolangs.org/w/index.php?diff=119822&oldid=105501 5* 03ChuckEsoteric08 5* (-9) 10
< 1700841374 900827 :cpressey!~cpressey@host-89-240-119-39.as13285.net QUIT :Quit: Client closed
< 1700842546 795767 :cpressey!~cpressey@host-89-240-119-39.as13285.net JOIN #esolangs cpressey :[https://web.libera.chat] cpressey
< 1700843137 152224 :riv!river@tilde.team/user/river PRIVMSG #esolangs :I think if you are trying to prove A |- Z   (You hvae the assumption A and want to prove B)
< 1700843149 520119 :riv!river@tilde.team/user/river PRIVMSG #esolangs :a forward proof step would be using A -> B to change your goal to proving B |- Z
< 1700843167 599517 :riv!river@tilde.team/user/river PRIVMSG #esolangs :and a backward proof step would be using Y -> Z to change your goal into A |- Y
< 1700844050 104632 :Gustof3!~Gustof3@175.sub-174-215-145.myvzw.com JOIN #esolangs * :Gustof3
< 1700844051 816531 :Koen!~Koen@78.199.192.3 QUIT :Remote host closed the connection
< 1700845644 492750 :Gustof3!~Gustof3@175.sub-174-215-145.myvzw.com QUIT :Quit: Leaving
< 1700846744 736317 :cpressey!~cpressey@host-89-240-119-39.as13285.net QUIT :Ping timeout: 250 seconds
> 1700847472 149559 PRIVMSG #esolangs :14[[07Monkeys14]]4 M10 02https://esolangs.org/w/index.php?diff=119823&oldid=94835 5* 03PythonshellDebugwindow 5* (+25) 10Category
< 1700848425 781506 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
< 1700849394 178946 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl JOIN #esolangs * :Textual User
> 1700850655 340518 PRIVMSG #esolangs :14[[07Kak14]]4 10 02https://esolangs.org/w/index.php?diff=119824&oldid=119822 5* 03Quito0567 5* (+37) 10Must be turing complete
> 1700850715 357055 PRIVMSG #esolangs :14[[07Kak14]]4 10 02https://esolangs.org/w/index.php?diff=119825&oldid=119824 5* 03Quito0567 5* (-37) 10Undo revision 119824 by [[Special:Contributions/Quito0567|Quito0567]] ([[User talk:Quito0567|talk]]) i take that back
< 1700851135 488668 :Thelie!~Thelie@2a03:2260:300c:400:61bd:fe2e:1f3c:b90a JOIN #esolangs Thelie :Thelie
< 1700851145 969872 :Koen!~Koen@78.199.192.3 JOIN #esolangs * :Koen
< 1700852846 25275 :esolangs!~esolangs@techne.zem.fi QUIT :Ping timeout: 245 seconds
< 1700852885 236853 :esolangs1!~esolangs@techne.zem.fi JOIN #esolangs esolangs :esolangs.org
< 1700852885 275566 :ChanServ!ChanServ@services.libera.chat MODE #esolangs +v :esolangs1
< 1700852999 244418 :esolangs1!~esolangs@techne.zem.fi NICK :esolangs
< 1700854287 546405 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :fungot, are cosmic rays actually cartridge fish, or are they just named after some superficial similarity?
< 1700854316 9423 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :hmm, our mascot isn't here
< 1700854575 179252 :fizzie!irc@selene.zem.fi PRIVMSG #esolangs :Oh.
< 1700854710 423732 :fizzie!irc@selene.zem.fi PRIVMSG #esolangs :Oh²: I updated it to expect the ~ in my hostname when I had that identd issue, which is now resolved (at least temporarily, after a Debian upgrade and reboot), so now it again doesn't acknowledge my authority in commanding it to join here.
< 1700854781 237900 :fungot!~fungot@2a01:4b00:82bb:1341::a JOIN #esolangs fungot :fungot-0.1
< 1700854791 718439 :int-e!~noone@int-e.eu PRIVMSG #esolangs :^style
< 1700854791 737080 :fungot!~fungot@2a01:4b00:82bb:1341::a PRIVMSG #esolangs :Available: agora alice c64 ct darwin discworld elon enron europarl ff7 fisher fungot homestuck ic irc* iwcs jargon lovecraft nethack oots pa qwantz sms speeches ss wp ukparl youtube
< 1700854841 956991 :SGautam!uid286066@id-286066.ilkley.irccloud.com JOIN #esolangs SGautam :Siddharth Gautam
< 1700855645 354509 :Thelie!~Thelie@2a03:2260:300c:400:61bd:fe2e:1f3c:b90a QUIT :Remote host closed the connection
< 1700856538 115386 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :fungot, are cosmic rays actually cartridge fish, or are they just named after some superficial similarity?
< 1700856538 788374 :fungot!~fungot@2a01:4b00:82bb:1341::a PRIVMSG #esolangs :b_jonas: nothing new? spill it) and it is slower then not creating it :)
< 1700857320 252188 :Sgeo!~Sgeo@user/sgeo JOIN #esolangs Sgeo :realname
< 1700857602 902452 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :fungot, out of these creatures, which two are what the second word of their name indicates? sea anemone, sea angel, sea ape, sea asparagus, sea bear, sea canary, sea cucumber, sea devil, sea elephant, sea fig, sea hare, sea hawk, sea horse, sea leopard, sea lettuce, sea lilies, sea lion, sea louse, sea moth, sea otter, sea porcupine, sea pork, sea raven, sea toad, sea unicorn, sea urchin, sea vomit, sea 
< 1700857603 203479 :fungot!~fungot@2a01:4b00:82bb:1341::a PRIVMSG #esolangs :b_jonas: i'm looking at gauche to teach myself lots of capsaicin today.
< 1700857608 915828 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :walnut, sea wasp.
< 1700857819 880213 :int-e!~noone@int-e.eu PRIVMSG #esolangs :"teach myself lots of capsaicin" sounds hot
< 1700857826 880565 :int-e!~noone@int-e.eu PRIVMSG #esolangs :(not in a sexual way)
< 1700857891 411058 :fizzie!irc@selene.zem.fi PRIVMSG #esolangs :Possibly relates to sea chilli peppers somehow.
< 1700857966 496533 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :nah, statistically speaking based on these creatures, sea chili peppers have nothing to do with chili peppers and don't contain capsaicin
< 1700858073 321478 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :admittedly I was a bit biased when I made that list, I took every name with the referent unrelated to the referent of the second word that I could find, even obsolete names that nobody uses anymore, while I took only two of the twenty or so examples where "sea" is a restricting suffix
< 1700858229 414242 :b_jonas!~x@89.134.28.161 PRIVMSG #esolangs :what complicates the matter is that "pepper" is already used for two entirely different groups of plants, one from each side of the ocean
< 1700859570 754713 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name)
< 1700860022 214404 :ais523!~ais523@user/ais523 QUIT :Quit: quit
< 1700864048 738380 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :possibly of interest to ppl here: updated version of earlier article at https://tromp.github.io/blog/2023/11/24/largest-number
< 1700864079 205583 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl PRIVMSG #esolangs :feedback welcome
< 1700864574 497959 :Koen!~Koen@78.199.192.3 QUIT :Quit: Leaving...
> 1700864897 88792 PRIVMSG #esolangs :14[[07Lazy Prefix14]]4 M10 02https://esolangs.org/w/index.php?diff=119826&oldid=34324 5* 03PythonshellDebugwindow 5* (+31) 10Category
> 1700865325 811376 PRIVMSG #esolangs :14[[07User:0ptr14]]4 M10 02https://esolangs.org/w/index.php?diff=119827&oldid=119641 5* 03None1 5* (-117) 10It is recommended to use interal links rather than external links for in-esolang links.
< 1700865439 763507 :tromp!~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl QUIT :Quit: My iMac has gone to sleep. ZZZzzz…
> 1700866433 739053 PRIVMSG #esolangs :14[[07Numeric Batch14]]4 M10 02https://esolangs.org/w/index.php?diff=119828&oldid=75777 5* 03PythonshellDebugwindow 5* (+63) 10See also, category
> 1700866762 258800 PRIVMSG #esolangs :14[[07MaybeNumericBatch14]]4 M10 02https://esolangs.org/w/index.php?diff=119829&oldid=39054 5* 03PythonshellDebugwindow 5* (+92) 10Stub, link, categories
> 1700866779 766717 PRIVMSG #esolangs :14[[07MaybeNumericBatch14]]4 M10 02https://esolangs.org/w/index.php?diff=119830&oldid=119829 5* 03PythonshellDebugwindow 5* (+14) 10Fix link
< 1700867326 623778 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name)
< 1700867703 999170 :SoniEx2!~quassel@sodapop.autistic.space NICK :Soni
< 1700867890 134060 :ais523!~ais523@user/ais523 QUIT :Quit: sorry about my connection
< 1700867903 246851 :ais523!~ais523@user/ais523 JOIN #esolangs ais523 :(this is obviously not my real name)
< 1700868002 90963 :SGautam!uid286066@id-286066.ilkley.irccloud.com QUIT :Quit: Connection closed for inactivity
< 1700869177 334996 :__monty__!~toonn@user/toonn QUIT :Quit: leaving