-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Archive Bot
committed
Apr 30, 2024
0 parents
commit e49fbda
Showing
20,567 changed files
with
1,307,499 additions
and
0 deletions.
The diff you're trying to view is too large. We only load the first 3000 changed files.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,20 @@ | ||
| on: | ||
| schedule: | ||
| - cron: '0 */4 * * *' | ||
|
|
||
| jobs: | ||
| publish_archive_job: | ||
| runs-on: ubuntu-latest | ||
| name: A job to publish zulip-archive in GitHub pages | ||
| steps: | ||
| - name: Checkout | ||
| uses: actions/checkout@v3 | ||
| - name: Run archive | ||
| id: archive | ||
| uses: zulip/zulip-archive@master | ||
| with: | ||
| zulip_organization_url: ${{ secrets.zulip_organization_url }} | ||
| zulip_bot_email: ${{ secrets.zulip_bot_email }} | ||
| zulip_bot_key: ${{ secrets.zulip_bot_key }} | ||
| github_token: ${{ secrets.GITHUB_TOKEN }} | ||
| delete_history: true |
Empty file.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,42 @@ | ||
| <html> | ||
| <head><meta charset="utf-8"><title>Zulip Chat Archive</title></head> | ||
| <hr> | ||
|
|
||
| <h2>Streams:</h2> | ||
|
|
||
| <ul> | ||
| <li> <a href="stream/336180-Archive-Mirror.3A-Isabelle-Users-Mailing-List/index.html">Archive Mirror: Isabelle Users Mailing List</a> (6817 topics) </li> | ||
|
|
||
| <li> <a href="stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/index.html">Mirror: Isabelle Users Mailing List</a> (1522 topics) </li> | ||
|
|
||
| <li> <a href="stream/238552-Beginner-Questions/index.html">Beginner Questions</a> (717 topics) </li> | ||
|
|
||
| <li> <a href="stream/202961-General/index.html">General</a> (285 topics) </li> | ||
|
|
||
| <li> <a href="stream/247542-Mirror.3A-Isabelle-Development-Mailing-List/index.html">Mirror: Isabelle Development Mailing List</a> (203 topics) </li> | ||
|
|
||
| <li> <a href="stream/211483-Isabelle.2FML/index.html">Isabelle/ML</a> (68 topics) </li> | ||
|
|
||
| <li> <a href="stream/214136-Announcements/index.html">Announcements</a> (33 topics) </li> | ||
|
|
||
| <li> <a href="stream/202968-quantum-computing/index.html">quantum computing</a> (22 topics) </li> | ||
|
|
||
| <li> <a href="stream/285459-Is-there-code-for-X.3F/index.html">Is there code for X?</a> (21 topics) </li> | ||
|
|
||
| <li> <a href="stream/202967-New-Members-.26-Projects/index.html">New Members & Projects</a> (15 topics) </li> | ||
|
|
||
| <li> <a href="stream/245944-Proof-Ground/index.html">Proof Ground</a> (7 topics) </li> | ||
|
|
||
| <li> <a href="stream/285806-SErAPIS/index.html">SErAPIS</a> (6 topics) </li> | ||
|
|
||
| <li> <a href="stream/203204-Machine-Learning-for-Isabelle/index.html">Machine Learning for Isabelle</a> (5 topics) </li> | ||
|
|
||
| <li> <a href="stream/211306-Lie/index.html">Lie</a> (3 topics) </li> | ||
|
|
||
| <li> <a href="stream/282466-IRC-.23isabelle/index.html">IRC #isabelle</a> (2 topics) </li> | ||
|
|
||
| <li> <a href="stream/336168-EMail-Test/index.html">EMail Test</a> (1 topic) </li> | ||
| </ul> | ||
|
|
||
| <hr><p>Last updated: Apr 30 2024 at 08:19 UTC</p> | ||
| </html> |
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,6 @@ | ||
| <?xml version="1.0" encoding="UTF-8"?> | ||
| <sitemapindex xmlns="http://www.sitemaps.org/schemas/sitemap/0.9"> | ||
| <!-- Powered by https://github.com/pigs-will-fly/py-xml-sitemap-writer --> | ||
| <!-- 1207 urls --> | ||
| <sitemap><loc>http://isabelle.systems/zulip-archive/sitemap-001-pages.xml.gz</loc></sitemap> | ||
| </sitemapindex> |
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,19 @@ | ||
| <html> | ||
| <head><meta charset="utf-8"><title>(no topic) · General · Zulip Chat Archive</title></head> | ||
| <h2>Stream: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/index.html">General</a></h2> | ||
| <h3>Topic: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/(no.20topic).html">(no topic)</a></h3> | ||
|
|
||
| <hr> | ||
|
|
||
| <base href="https://isabelle.zulipchat.com/"> | ||
|
|
||
| <head><link href="http://isabelle.systems/zulip-archive/style.css" rel="stylesheet"></head> | ||
|
|
||
| <a name="262744558"></a> | ||
| <h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%28no%20topic%29/near/262744558" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Simon Wimmer <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/(no.20topic).html#262744558">(Nov 25 2021 at 22:21)</a>:</h4> | ||
| <p>Ah nice! I'll ask him about it.</p> | ||
|
|
||
|
|
||
|
|
||
| <hr><p>Last updated: Jul 15 2022 at 23:21 UTC</p> | ||
| </html> |
173 changes: 173 additions & 0 deletions
173
...m/202961-General/topic/.22Real.22.20imperative.20code.20generation.20from.20Isabelle.html
Large diffs are not rendered by default.
Oops, something went wrong.
36 changes: 36 additions & 0 deletions
36
...8How.29.20can.20I.20declare.20a.20domain.20a.20codatatype.20.28or.20vice-versa.29.3F.html
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,36 @@ | ||
| <html> | ||
| <head><meta charset="utf-8"><title>(How) can I declare a domain a codatatype (or vice-versa)? · General · Zulip Chat Archive</title></head> | ||
| <h2>Stream: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/index.html">General</a></h2> | ||
| <h3>Topic: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.28How.29.20can.20I.20declare.20a.20domain.20a.20codatatype.20.28or.20vice-versa.29.3F.html">(How) can I declare a domain a codatatype (or vice-versa)?</a></h3> | ||
|
|
||
| <hr> | ||
|
|
||
| <base href="https://isabelle.zulipchat.com/"> | ||
|
|
||
| <head><link href="http://isabelle.systems/zulip-archive/style.css" rel="stylesheet"></head> | ||
|
|
||
| <a name="423359816"></a> | ||
| <h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%28How%29%20can%20I%20declare%20a%20domain%20a%20codatatype%20%28or%20vice-versa%29%3F/near/423359816" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Max Baumann <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.28How.29.20can.20I.20declare.20a.20domain.20a.20codatatype.20.28or.20vice-versa.29.3F.html#423359816">(Feb 26 2024 at 09:51)</a>:</h4> | ||
| <p>I have a domain declared somewhat like this:</p> | ||
| <div class="codehilite" data-code-language="Isabelle"><pre><span></span><code><span class="k">domain</span><span class="w"> </span><span class="o">(</span><span class="n n-Type">'a</span><span class="w"> </span><span class="o">::</span><span class="w"> </span><span class="s">"domain"</span><span class="o">)</span><span class="w"> </span><span class="n">llist</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">LCons</span><span class="w"> </span><span class="o">(</span><span class="n">lhd</span><span class="o">::</span><span class="s">"'a"</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="kp">lazy</span><span class="w"> </span><span class="n">ltl</span><span class="o">::</span><span class="s">"'a llist"</span><span class="o">)</span> | ||
| </code></pre></div> | ||
| <p>Can I additionally make this a codatatype, like this?</p> | ||
| <div class="codehilite" data-code-language="Isabelle"><pre><span></span><code><span class="k">codatatype</span><span class="w"> </span><span class="n n-Type">'a</span><span class="w"> </span><span class="n">llist</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">lbot</span><span class="o">:</span><span class="n">LNil</span><span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">LCons</span><span class="o">(</span><span class="n">lhd</span><span class="o">:</span><span class="n n-Type">'a</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">ltl</span><span class="o">:</span><span class="s">"'a llist"</span><span class="o">)</span> | ||
| </code></pre></div> | ||
|
|
||
|
|
||
|
|
||
| <a name="423410897"></a> | ||
| <h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%28How%29%20can%20I%20declare%20a%20domain%20a%20codatatype%20%28or%20vice-versa%29%3F/near/423410897" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Manuel Eberl <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.28How.29.20can.20I.20declare.20a.20domain.20a.20codatatype.20.28or.20vice-versa.29.3F.html#423410897">(Feb 26 2024 at 14:45)</a>:</h4> | ||
| <p>What is a "domain"? Are you using some special package?</p> | ||
|
|
||
|
|
||
|
|
||
| <a name="423412099"></a> | ||
| <h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%28How%29%20can%20I%20declare%20a%20domain%20a%20codatatype%20%28or%20vice-versa%29%3F/near/423412099" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Max Baumann <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.28How.29.20can.20I.20declare.20a.20domain.20a.20codatatype.20.28or.20vice-versa.29.3F.html#423412099">(Feb 26 2024 at 14:50)</a>:</h4> | ||
| <p>Sorry, forgot to mention it. It's a HOLCF domain.</p> | ||
|
|
||
|
|
||
|
|
||
| <hr><p>Last updated: Apr 30 2024 at 08:19 UTC</p> | ||
| </html> |
32 changes: 32 additions & 0 deletions
32
stream/202961-General/topic/.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,32 @@ | ||
| <html> | ||
| <head><meta charset="utf-8"><title>`quick_and_dirty` mode skips regular proofs · General · Zulip Chat Archive</title></head> | ||
| <h2>Stream: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/index.html">General</a></h2> | ||
| <h3>Topic: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html">`quick_and_dirty` mode skips regular proofs</a></h3> | ||
|
|
||
| <hr> | ||
|
|
||
| <base href="https://isabelle.zulipchat.com/"> | ||
|
|
||
| <head><link href="http://isabelle.systems/zulip-archive/style.css" rel="stylesheet"></head> | ||
|
|
||
| <a name="272252199"></a> | ||
| <h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%60quick_and_dirty%60%20mode%20skips%20regular%20proofs/near/272252199" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Fabian Huch <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html#272252199">(Feb 17 2022 at 12:33)</a>:</h4> | ||
| <p>When <code>quick_and_dirty</code> mode is enabled, some regular proofs get replaced with skip proofs (i.e. <code>sorry</code> oracles). For example, the following will throw an Exception when you <code>build</code> it (curiously, the interactive session works just fine):</p> | ||
| <div class="codehilite" data-code-language="Isabelle"><pre><span></span><code><span class="k">fun</span> <span class="n">ex</span> <span class="o">::</span> <span class="s">"'a ⇒ nat"</span> <span class="kp">where</span> | ||
| <span class="s">"ex _ = 0"</span> | ||
|
|
||
| <span class="kn">theorem</span> <span class="n">ex_const</span><span class="o">:</span> <span class="s">"ex 5 = ex 7"</span> | ||
| <span class="k">by</span> <span class="n">auto</span> | ||
|
|
||
| <span class="k">ML</span> <span class="err">‹</span> | ||
| <span class="n">exception</span> <span class="n">E</span><span class="err">;</span> | ||
| <span class="kp">if</span> <span class="o">(</span><span class="n">Thm_Deps.has_skip_proof</span> <span class="o">[</span><span class="err">@</span><span class="ow">{</span><span class="kt">thm</span> <span class="n">ex_const</span><span class="ow">}</span><span class="o">])</span> <span class="k">then</span> <span class="n">raise</span> <span class="n">E</span> | ||
| <span class="n">else</span> <span class="o">()</span> | ||
| <span class="err">›</span> | ||
| </code></pre></div> | ||
| <p>Is there a reason for that? Or an option to disable this behavior?</p> | ||
|
|
||
|
|
||
|
|
||
| <hr><p>Last updated: Jul 15 2022 at 23:21 UTC</p> | ||
| </html> |
41 changes: 41 additions & 0 deletions
41
stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,41 @@ | ||
| <html> | ||
| <head><meta charset="utf-8"><title>`rewrite` method tutorial · General · Zulip Chat Archive</title></head> | ||
| <h2>Stream: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/index.html">General</a></h2> | ||
| <h3>Topic: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html">`rewrite` method tutorial</a></h3> | ||
|
|
||
| <hr> | ||
|
|
||
| <base href="https://isabelle.zulipchat.com/"> | ||
|
|
||
| <head><link href="http://isabelle.systems/zulip-archive/style.css" rel="stylesheet"></head> | ||
|
|
||
| <a name="191468106"></a> | ||
| <h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%60rewrite%60%20method%20tutorial/near/191468106" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Chen <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html#191468106">(Mar 23 2020 at 12:54)</a>:</h4> | ||
| <p>I seem to recall that there was a PDF tutorial describing the <code>rewrite</code> method, does anyone know where it lives?</p> | ||
|
|
||
|
|
||
|
|
||
| <a name="191475114"></a> | ||
| <h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%60rewrite%60%20method%20tutorial/near/191475114" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Kevin Kappelmann <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html#191475114">(Mar 23 2020 at 13:51)</a>:</h4> | ||
| <p>Only thing I found is <a href="https://pdfs.semanticscholar.org/717e/4d3dbf9fe5fdef35df1c91152f1bd04d9b63.pdf" target="_blank" title="https://pdfs.semanticscholar.org/717e/4d3dbf9fe5fdef35df1c91152f1bd04d9b63.pdf">the paper</a> describing the subterm selection part of the tactic, but I guess that's not what you were looking for</p> | ||
|
|
||
|
|
||
|
|
||
| <a name="191475265"></a> | ||
| <h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%60rewrite%60%20method%20tutorial/near/191475265" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Chen <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html#191475265">(Mar 23 2020 at 13:52)</a>:</h4> | ||
| <p>Mm yeah I found that too, but somehow I have this memory of reading an actual tutorial for <code>rewrite</code>. Thanks though! :)</p> | ||
|
|
||
|
|
||
|
|
||
| <a name="191655242"></a> | ||
| <h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%60rewrite%60%20method%20tutorial/near/191655242" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Simon Wimmer <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.60rewrite.60.20method.20tutorial.html#191655242">(Mar 24 2020 at 18:42)</a>:</h4> | ||
| <p><span class="user-mention silent" data-user-id="233154">Kevin Kappelmann</span> <a href="#narrow/stream/202961-general/topic/.60rewrite.60.20method.20tutorial/near/191475114" title="#narrow/stream/202961-general/topic/.60rewrite.60.20method.20tutorial/near/191475114">said</a>:</p> | ||
| <blockquote> | ||
| <p>Only thing I found is <a href="https://pdfs.semanticscholar.org/717e/4d3dbf9fe5fdef35df1c91152f1bd04d9b63.pdf" target="_blank" title="https://pdfs.semanticscholar.org/717e/4d3dbf9fe5fdef35df1c91152f1bd04d9b63.pdf">the paper</a> describing the subterm selection part of the tactic, but I guess that's not what you were looking for</p> | ||
| </blockquote> | ||
| <p>Yes, I think this is the only source.</p> | ||
|
|
||
|
|
||
|
|
||
| <hr><p>Last updated: Apr 30 2024 at 08:19 UTC</p> | ||
| </html> |
40 changes: 40 additions & 0 deletions
40
....9C.94.20.60.5C.3Ccomment.3E.60.20after.20.60text.60.20omitted.20in.20LaTeX.20output.html
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,40 @@ | ||
| <html> | ||
| <head><meta charset="utf-8"><title>✔ `\<comment>` after `text` omitted in LaTeX output · General · Zulip Chat Archive</title></head> | ||
| <h2>Stream: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/index.html">General</a></h2> | ||
| <h3>Topic: <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.E2.9C.94.20.60.5C.3Ccomment.3E.60.20after.20.60text.60.20omitted.20in.20LaTeX.20output.html">✔ `\<comment>` after `text` omitted in LaTeX output</a></h3> | ||
|
|
||
| <hr> | ||
|
|
||
| <base href="https://isabelle.zulipchat.com/"> | ||
|
|
||
| <head><link href="http://isabelle.systems/zulip-archive/style.css" rel="stylesheet"></head> | ||
|
|
||
| <a name="270589789"></a> | ||
| <h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%E2%9C%94%20%60%5C%3Ccomment%3E%60%20after%20%60text%60%20omitted%20in%20LaTeX%20output/near/270589789" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Max Jakobitsch <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.E2.9C.94.20.60.5C.3Ccomment.3E.60.20after.20.60text.60.20omitted.20in.20LaTeX.20output.html#270589789">(Feb 03 2022 at 17:48)</a>:</h4> | ||
| <p>Marginal comments (<code>\<comment></code>) normally are part of the LaTeX/PDF output, but are left out when they appear after <code>text</code> (and some other markup commands I have tried).</p> | ||
| <div class="codehilite" data-code-language="Isabelle"><pre><span></span><code><span class="kt">term</span> <span class="n">A</span> | ||
|
|
||
| <span class=" -Symbol">\<comment></span> <span class=" -Symbol">\<open></span><span class="n">Marginal</span> <span class="n">comments</span> <span class="n">should</span> <span class="n">appear</span> <span class="kp">in</span> <span class="n">LaTeX</span><span class="o">,</span> <span class="n">right</span><span class="o">?</span><span class=" -Symbol">\<close></span> | ||
|
|
||
| <span class="k">text</span><span class=" -Symbol">\<open></span><span class="n">But</span> <span class="n">apparently</span> <span class="n">not</span> <span class="n">after</span> <span class="n">markup</span> <span class="n">commands.</span><span class=" -Symbol">\<close></span> | ||
|
|
||
| <span class=" -Symbol">\<comment></span> <span class=" -Symbol">\<open></span><span class="n">I'm</span> <span class="n">invisible</span><span class="o">!</span><span class=" -Symbol">\<close></span> | ||
| </code></pre></div> | ||
| <p>Is this intended behavior?</p> | ||
|
|
||
|
|
||
|
|
||
| <a name="270592317"></a> | ||
| <h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%E2%9C%94%20%60%5C%3Ccomment%3E%60%20after%20%60text%60%20omitted%20in%20LaTeX%20output/near/270592317" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Manuel Eberl <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.E2.9C.94.20.60.5C.3Ccomment.3E.60.20after.20.60text.60.20omitted.20in.20LaTeX.20output.html#270592317">(Feb 03 2022 at 18:05)</a>:</h4> | ||
| <p>Sounds like it's not intended. It's best to report such things directly to the isabelle-users mailing list. This is something Makarius should know about, and he doesn't read Zulip.</p> | ||
|
|
||
|
|
||
|
|
||
| <a name="270593521"></a> | ||
| <h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%E2%9C%94%20%60%5C%3Ccomment%3E%60%20after%20%60text%60%20omitted%20in%20LaTeX%20output/near/270593521" class="zl"><img src="http://isabelle.systems/zulip-archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Notification Bot <a href="http://isabelle.systems/zulip-archive/stream/202961-General/topic/.E2.9C.94.20.60.5C.3Ccomment.3E.60.20after.20.60text.60.20omitted.20in.20LaTeX.20output.html#270593521">(Feb 03 2022 at 18:14)</a>:</h4> | ||
| <p><span class="user-mention silent" data-user-id="407560">Max Jakobitsch</span> has marked this topic as resolved.</p> | ||
|
|
||
|
|
||
|
|
||
| <hr><p>Last updated: Apr 30 2024 at 08:19 UTC</p> | ||
| </html> |
Oops, something went wrong.