文章/答案/技术大牛

发布

社区首页 >问答首页 >如何在根中指定非文档理论文件？

问如何在根中指定非文档理论文件？
EN

Stack Overflow用户

提问于 2014-07-25 05:41:11

回答 2查看 276关注 0票数 0

我将Nominal2导入到我的主要理论文件中，而在Isabelle/jEdit中，我可以使用atom_decl来工作。在根用户中，我尝试了各种尝试来指定Nominal2，如

session "techreport" = "HOL" + 
   options [document = pdf, document_output = "output"] 
   theories [document = false] 
     Nominal2 
   theories 
     IsarIntroduction 
   files "document/root.tex"

但我得到了bad input或No such file: "Nominal2.thy"。我试图从IsarIntroduction的dir和root.tex的dir指定一个相对路径，但都是徒劳的。

如何为Nominal2理论指定路径？

更新:我使用了一个专门为Isabelle/JEdit构建的Nominal2映像

isabelle

回答 2

Stack Overflow用户

回答已采纳

发布于 2014-08-02 03:57:34

您还应该能够构建会话(图像) Nominal2，就像在Isabelle/jEdit中所做的那样。例如：

session "techreport" = "Nominal2" + 
   options [document = pdf, document_output = "output"] 
   theories 
     IsarIntroduction 
   files "document/root.tex"

票数 1

Stack Overflow用户

发布于 2014-07-25 10:24:12

有人摆弄我找到了解决办法。

No such file: "Nominal2.thy"消息来自于isabelle build进程，它没有看到伊莎贝尔/jEdit使用的带有Nominal2的预构建映像。因此，给出了Nominal2在主理论文件IsarIntroduction.thy和ROOT文件中的完整路径，解决了该问题。

但是有一个警告:我得到了一个超过200页的文档，其中包含了Infinite_Set.thy的所有开发。原木

Loading theory "Infinite_Set" (required by "IsarIntroduction" 
via "Nominal2" via "Nominal2_Base")

所以我不得不包括

theories [document = false]
  "Nominal2-Isabelle2013-1/Nominal/Nominal2"
  "~~/src/HOL/Library/Infinite_Set"

在ROOT中防止这种情况发生。

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/24957145

复制

C++ 中的随机标头系列1

编程算法

开启掘金成长之旅！这是我参与「掘金日新计划 · 12 月更文挑战」的第1天，点击查看活动详情

鲸落c

2022/11/28

1.3K0

通过 HTTP 标头的 XSS

http 网络安全 php 编程算法缓存

在某些情况下，在应用程序的一个 HTTP 标头中传递的信息未正确清理，并在请求页面的某处或另一端输出，从而导致 XSS 情况。

Khan安全团队

2022/03/09

2.1K0

通过主机标头的 XSS

php go html https

在 IE 中处理重定向时有一个有趣的错误，它可以将任意字符插入到 Host 标头中。假设您有以下 http 响应：

Khan安全团队

2022/01/11

1.6K0

常见的HTTP标头介绍

http 爬虫

在网络爬虫的实践过程中会遇到诸多挑战，被屏蔽是最令人头疼的一个。幸好，有许多技术可以帮助您免受IP屏蔽带来的影响，这其中，HTTP标头（HTTP Headers）的使用和优化是最有效的方法之一，但它往往也是最被大家低估的方法之一。

用户7850017

2022/05/07

1.1K0

设置和获取HTTP标头

http 网络安全编程算法

%Net.HttpRequest的以下每个属性都包含具有相应名称的HTTP标头的值。如果不设置这些属性，则会自动计算它们：

用户7741497

2022/06/09

2.5K0

Repeater嵌套DataList

java https 网络安全

发布者：全栈程序员栈长，转载请注明出处：https://javaforall.cn/159134.html原文链接：https://javaforall.cn

全栈程序员站长

2022/09/14

4260

datalist标签小结

javascript

在Web设计中,经常会用到如输入框的自动下拉提示,这将大大方便用户的输入。在以前，如果要实现这样的功能，必须要求开发者使用一些Javascript的技巧或相关的框架进行ajax调用，需要一定的编程工作量。但随着HTML5 的慢慢普及，开发者可以使用其中的新的DataList标记就能快速开发出十分漂亮的 AutoComplete组件的效果一、datalist标签的使用示例 HTML 代码复制 <!DOCTYPE html> <html> <head> <title>HTML5 data

吴裕超

2018/02/28

2.5K0

DataList分页

asp html java 编程算法

<% @ Import Namespace="System.Data.OleDb" %>

Java架构师必看

2021/03/22

4150

Log4Shell HTTP 标头注入

https 网络安全 html

此模块需要 Metasploit：https://metasploit.com/download

Khan安全团队

2022/01/14

1.1K0

「HTTP标头」都给你整理好了

缓存 http https 网络安全

HTTP 1.1 的标头主要分为四种，通用标头、实体标头、请求标头、响应标头，现在我们来对这几种标头进行介绍

Java3y

2020/02/19

5.8K0

使用结构化的标头字段改善HTTP

http 文件存储网站 cdn

原文 / https://www.fastly.com/blog/improve-http-structured-headers

LiveVideoStack

2020/08/04

6550

基于内容的图像检索技术：从特征到检索

数据库 sql 编程算法

构建词库是离线操作，主要对目标数据集中的文本进行解析提取词干信息，建立当前数据集的词库，然后基于词库，对数据集中所有文档提取本文特征。构建词库在整个检索系统生命周期开始阶段实施，一般情况仅执行一次，是针对目标检索文本数据集进行的非频繁性操作。

公众号机器学习与AI生成创作

2020/12/08

1.6K0

服务器未能识别 HTTP 标头 SOAPAction 的值

.net http

SOAPAction HTTP request header被用来标识SOAP HTTP请求的目的地，其值是个URI地址。SOAP发送并不限制格式、URI特征或其必须可解析，那么在这种情况下，发送一个HTTP SOAP请求时，其HTTP客户端必须使用/指明SOAPAction HTTP request header。 SOAPAction header的内容可以被用在服务端，诸如：防火墙适当的过滤基于HTTP的SOAP请求消息等场景。SOAPAction header的值为空串("")表示SOAP消息的目

张善友

2018/01/19

3K0

Repeater,DataList,DataGrid

datagrid repeater 分页

输出表： string a="Provider=Microsoft.Jet.OLEDB.4.0;Data Source=c:\\data.mdb;Persist Security Info=False;"; OleDbConnection cn=new OleDbConnection(a); OleDbCommand cm=new OleDbCommand("select * from test2",cn); cn.Open(); OleDbDataReader

用户1075292

2018/01/23

7740

改进 Elastic Stack 中的信息检索：混合检索

Elasticsearch Service

在我们的上一篇博文中，我们介绍了 Elastic Learned Sparse Encoder，这是一种经过训练可有效进行零样本文本检索的模型。Elasticsearch ®还具有强大的词汇检索功能和丰富的工具来组合不同查询的结果。在本博客中，我们介绍了混合检索的概念，并探讨了 Elasticsearch 中可用的两种具体实现。特别是，我们探索如何通过使用倒数排名融合和加权分数和将弹性学习稀疏编码器与 BM25 相结合来提高其性能。

点火三周

2023/07/20

2.1K0

H5标签datalist

https 网络安全

有的时候前端为了更好地实现输入框input的交互效果，需要增加搜索联想功能，除了使用已经封装好的组件或者自己手写js以外，我们可以使用datalist标签更简便地去实现这个功能。

全栈程序员站长

2022/11/16

6770

在Asp.Net中从sqlserver检索(retrieve)图片

sql 数据库 java 编程算法

介绍：这篇文章是我写的"如何把图片存入sqlServer中"的后续。我建议你在读这篇文章之前先看看那篇。和存储图片相比，读取图片就要简单多了。输出一副图片我们要做的就是使用Response对象的BinaryWrite方法。同时设置图片的格式。在这篇文章中，我们将讨论如何从SqlServer中检索图片。并将学习以下几个方面的知识. ·如何设置图片的格式？ ·如何使用BinaryWrite方法。

Java架构师必看

2021/03/22

1.5K0

C# Datalist 多列及Image中图片路径的绑定

asp actionscript

今天搞公司三放心员工评选的程序，最后的评选是那种带头像，下面是评选星级和点赞的那种，平常的都是数据管理，用Gridview比较多，今天学习和尝试多列的绑定可以使用Repeater，也可以用Datalist。我最后用了Datalist，简单好用。整理到这里，备自己以后用。

崔文远TroyCui

2019/02/26

1.5K0

从mybatis sql模板中获取参数信息

mybatis sql xml 网络安全

最近在尝试从mybatis sql模板中获取参数信息，期间学习了mybatis内部的一些结构，接下来笔者就向大家分享mybatis相关知识和具体代码实现。

zhangheng

2021/01/12

7.8K0

从0到1快速了解ElasticSearch数据检索

Elasticsearch Service nosql 存储

这篇文章主要讨论一下ElasticSearch数据检索内部流程，方便大家对数据检索的理解。如果对ElasticSearch的文档写入不了解的同学可以先看一下上一篇文章【从0到1了解ElasticSearch文档写入】。

爱拼才会赢

2021/10/21

1.2K0

相似问题

如何使用javascript (如php foreach)在iframe中循环数组？

如何在javascript中中断foreach循环？

如何在javascript中跳出foreach循环

如何在Javascript中应用条件to forEach循环？

120

Javascript forEach循环

添加站长进交流群

领取专属 10元无门槛券

AI混元助手 在线答疑

关注 腾讯云开发者公众号

洞察 腾讯核心技术

剖析业界实践案例

问如何在根中指定非文档理论文件？
EN

回答 2

Stack Overflow用户

Stack Overflow用户

如何使用javascript (如php foreach)在iframe中循环数组？

如何在javascript中中断foreach循环？

如何在javascript中跳出foreach循环

如何在Javascript中应用条件to forEach循环？

Javascript forEach循环

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问如何在根中指定非文档理论文件？EN

回答 2

Stack Overflow用户

Stack Overflow用户

如何使用javascript (如php foreach)在iframe中循环数组？

如何在javascript中中断foreach循环？

如何在javascript中跳出foreach循环

如何在Javascript中应用条件to forEach循环？

Javascript forEach循环

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问如何在根中指定非文档理论文件？
EN