-
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
Feb 10, 2024
0 parents
commit 9b6a54e
Showing
20,185 changed files
with
1,283,679 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> (1427 topics) </li> | ||
|
||
<li> <a href="stream/238552-Beginner-Questions/index.html">Beginner Questions</a> (665 topics) </li> | ||
|
||
<li> <a href="stream/202961-General/index.html">General</a> (267 topics) </li> | ||
|
||
<li> <a href="stream/247542-Mirror.3A-Isabelle-Development-Mailing-List/index.html">Mirror: Isabelle Development Mailing List</a> (186 topics) </li> | ||
|
||
<li> <a href="stream/211483-Isabelle.2FML/index.html">Isabelle/ML</a> (64 topics) </li> | ||
|
||
<li> <a href="stream/214136-Announcements/index.html">Announcements</a> (29 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> (20 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: Feb 10 2024 at 16:18 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 --> | ||
<!-- 1129 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.
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: Feb 10 2024 at 16:18 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: Feb 10 2024 at 16:18 UTC</p> | ||
</html> |
44 changes: 44 additions & 0 deletions
44
...61-General/topic/.E2.9C.94.20.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,44 @@ | ||
<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/.E2.9C.94.20.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/%E2%9C%94%20%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/.E2.9C.94.20.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> | ||
|
||
|
||
|
||
<a name="272692571"></a> | ||
<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%E2%9C%94%20%60quick_and_dirty%60%20mode%20skips%20regular%20proofs/near/272692571" 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/.E2.9C.94.20.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html#272692571">(Feb 21 2022 at 14:07)</a>:</h4> | ||
<p>Apparently <code>quick_and_dirty</code> also axiomatizes some datatype/function constructions (so that they are faster), which is the reason the above fails. Except for locally disabling <code>quick_and_dirty</code>, there does not seem to be an option to turn that off.</p> | ||
|
||
|
||
|
||
<a name="272692596"></a> | ||
<h4><a href="https://isabelle.zulipchat.com/#narrow/stream/202961-General/topic/%E2%9C%94%20%60quick_and_dirty%60%20mode%20skips%20regular%20proofs/near/272692596" 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.60quick_and_dirty.60.20mode.20skips.20regular.20proofs.html#272692596">(Feb 21 2022 at 14:07)</a>:</h4> | ||
<p><span class="user-mention silent" data-user-id="348400">Fabian Huch</span> has marked this topic as resolved.</p> | ||
|
||
|
||
|
||
<hr><p>Last updated: Feb 10 2024 at 16:18 UTC</p> | ||
</html> |
Oops, something went wrong.