1591 Commits

All Branches

Search

Author	SHA1	Message	Date
Makarius Wenzel	d20e9ccd22	Proper session qualifier for theory imports (amending 44cae2e631)	2022-12-04 00:45:07 +01:00
Makarius Wenzel	f2ee5d3780	Tuned	2022-12-04 00:10:43 +01:00
Makarius Wenzel	44cae2e631	More formal management of ontologies in Isabelle/ML/Isar with output via Isabelle/Scala exports	2022-12-04 00:09:29 +01:00
Makarius Wenzel	7b2bf35353	More strict treatment of document export artifacts	2022-12-03 14:54:14 +01:00
Makarius Wenzel	e8c7fa6018	Clarified signature	2022-12-03 14:44:04 +01:00
Makarius Wenzel	b12e61511d	Discourage etc/options	2022-12-03 13:55:56 +01:00
Makarius Wenzel	3cac42e6cb	Clarified order	2022-12-03 12:39:00 +01:00
Makarius Wenzel	aee8ba1df1	Prefer DOF parameters over Isabelle options	2022-12-03 12:37:58 +01:00
Makarius Wenzel	d93e1383d4	Afford full-scale command-line tool	2022-12-03 12:29:24 +01:00
Makarius Wenzel	3d5d1e7476	Further attempts at woodpecker environment	2022-12-02 22:54:02 +01:00
Makarius Wenzel	4264e7cd15	Build Scala/Java components to get proper ISABELLE_CLASSPATH	2022-12-02 21:40:59 +01:00
Makarius Wenzel	96f4077c53	Tuned message	2022-12-02 21:29:45 +01:00
Makarius Wenzel	d7fb39d7eb	Adhoc command-line tool replaces old options	2022-12-02 21:14:55 +01:00
Makarius Wenzel	b95826962f	Tuned documentation	2022-12-02 20:29:40 +01:00
Makarius Wenzel	912d4bb49e	Maintain document template in Isabelle/ML via Isar commands: ... result becomes export artifact, which is harvested by Isabelle/Scala build engine	2022-12-02 20:05:15 +01:00
Makarius Wenzel	a6c1a2baa4	Removed obsolete "extend" operation	2022-12-02 15:31:23 +01:00
Makarius Wenzel	bb5963c6e2	Proper usage of dof_mkroot, although its Bash pretty-printing in LaTeX is a bit odd	2022-12-02 14:35:17 +01:00
Makarius Wenzel	cc3e2a51a4	More antiquotations	2022-12-02 13:50:16 +01:00
Makarius Wenzel	9e4e5b49eb	More antiquotations from Isabelle2021-1/2022	2022-12-02 11:41:31 +01:00
Makarius Wenzel	b65ecbdbef	Updated to Isabelle2022	2022-12-02 10:34:15 +01:00
Makarius Wenzel	3be2225dcf	Tuned comments	2022-12-01 22:54:01 +01:00
Makarius Wenzel	f44f0af01c	Use regular Toplevel.presentation from Isabelle2022, without alternative presentation hook	2022-12-01 22:48:45 +01:00
Makarius Wenzel	9a11baf840	Latex.output_name name is back in Isabelle2022	2022-12-01 22:04:56 +01:00
Makarius Wenzel	48c167aa23	Proper DOF.artifact_url	2022-12-01 21:45:06 +01:00
Makarius Wenzel	700a9bbfee	clarified DOF.options: hard-wired document_comment_latex always uses LaTeX version of comment.sty	2022-12-01 21:30:32 +01:00
Makarius Wenzel	73299941ad	Tuned	2022-12-01 17:26:29 +01:00
Makarius Wenzel	5a8c438c41	Omit excessive quotes	2022-12-01 16:48:33 +01:00
Makarius Wenzel	7772c73aaa	More accurate defaults	2022-12-01 16:39:41 +01:00
Makarius Wenzel	ca18453043	Clarified signature: more explicit types and operations	2022-12-01 16:28:44 +01:00
Makarius Wenzel	1a122b1a87	More robust default	2022-12-01 15:48:52 +01:00
Makarius Wenzel	47d95c467e	Tuned whitespace	2022-12-01 15:33:16 +01:00
Makarius Wenzel	bf3085d4c0	Clairifed defaults and command-line options	2022-12-01 15:26:48 +01:00
Makarius Wenzel	068e6e0411	Tuned	2022-12-01 14:23:00 +01:00
Makarius Wenzel	09e9980691	Tuned	2022-12-01 14:22:32 +01:00
Makarius Wenzel	94ce3fdec2	Prefer constants in Scala, to make this independent from component context	2022-12-01 14:15:17 +01:00
Makarius Wenzel	44819bff02	Updated message, following c29ec9641a	2022-12-01 12:44:03 +01:00
Makarius Wenzel	a6ab1e101e	Update Isabelle + AFP URLs	2022-12-01 11:55:51 +01:00
Makarius Wenzel	c29ec9641a	Simplified installation	2022-12-01 11:45:12 +01:00
Nicolas Méric	06833aa190	Upddate single argument handling for compute_attr_access ... Trigger error when the attribute is not specified as an argument of the antiquatation and is not an attribujte of the instance. (In these case, the position of the attribute is NONE)	2022-11-28 10:05:47 +01:00
Nicolas Méric	4f0c7e1e95	Fix type unification clash for trace_attribute term antiquotation	2022-11-25 08:57:59 +01:00
Nicolas Méric	0040949cf8	Add trace-attribute term antiquotation ... - Make doc_class type and constant used by regular expression in monitors ground - Make class tag attribute ground (with serial()) - The previous items make possible the evaluation of the trace attribute and the definition of the trace-attribute term annotation	2022-11-24 16:47:21 +01:00
Nicolas Méric	e68c332912	Fix markup for some antiquotations ... Fix markup for docitem_attribute and trace_attribute ML and text antiquotations	2022-11-24 11:22:02 +01:00
Burkhart Wolff	b2c4f40161	Some LaTeX experiments with Achim	2022-11-18 10:30:33 +01:00
Burkhart Wolff	309952e0ce	syntactic rearrangements	2022-11-09 11:19:00 +01:00
Burkhart Wolff	830e1b440a	ported another Figure* in OutOfOrderPresntn to Isabelle2022	2022-11-09 06:06:30 +01:00
Burkhart Wolff	2149db9efc	semantics of fig_content (untested)	2022-11-08 20:52:58 +01:00
Burkhart Wolff	1547ace64b	added some semantics to fig_content	2022-11-08 19:27:07 +01:00
Burkhart Wolff	39acd61dfd	Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF	2022-11-08 10:03:30 +01:00
Burkhart Wolff	29770b17ee	added syntax for fig_content	2022-11-08 10:03:15 +01:00
Achim D. Brucker	b4f4048cff	Made clear that more than two AFP entries are required.	2022-11-07 17:05:04 +00:00