diff options
author | Karl Berry <karl@freefriends.org> | 2023-09-05 20:05:11 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2023-09-05 20:05:11 +0000 |
commit | f886123ec8e5ba2e4ffe6ce9cd57a88a803ae502 (patch) | |
tree | 337b238cb20061c2217fdff6094ca1f1e194f330 | |
parent | b47027a7c4103e9c77f75e62761b446adcfb62fb (diff) |
fitch (5sep23)
git-svn-id: svn://tug.org/texlive/trunk@68179 c570f23f-e606-0410-a88d-b1316a301751
-rw-r--r-- | Master/texmf-dist/doc/latex/fitch/README.md | 82 | ||||
-rw-r--r-- | Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt | 314 | ||||
-rw-r--r-- | Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdf | bin | 0 -> 7325 bytes | |||
-rw-r--r-- | Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf | bin | 0 -> 248637 bytes | |||
-rw-r--r-- | Master/texmf-dist/doc/latex/fitch/fitchdoc.tex | 406 | ||||
-rw-r--r-- | Master/texmf-dist/doc/latex/fitch/fitchexample.png | bin | 0 -> 4727 bytes | |||
-rw-r--r-- | Master/texmf-dist/tex/latex/fitch/fitch.sty | 231 | ||||
-rwxr-xr-x | Master/tlpkg/bin/tlpkg-ctan-check | 2 | ||||
-rw-r--r-- | Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc | 1 | ||||
-rw-r--r-- | Master/tlpkg/tlpsrc/fitch.tlpsrc | 0 |
10 files changed, 1035 insertions, 1 deletions
diff --git a/Master/texmf-dist/doc/latex/fitch/README.md b/Master/texmf-dist/doc/latex/fitch/README.md new file mode 100644 index 00000000000..1208f4f2dd2 --- /dev/null +++ b/Master/texmf-dist/doc/latex/fitch/README.md @@ -0,0 +1,82 @@ +# fitch.sty + +LaTeX macros for Fitch style natural deduction + +## Usage + +Fitch-style natural deduction is a system for writing proofs in +propositional logic and predicate logic. This is a set of easy-to-use +LaTeX macros originally written by Peter Selinger. It is used, e.g., +in the various versions of _forall x_ by PD Magnus (e.g., the [original](https://www.fecundity.com/logic/download.html), +[Cambridge](http://www.homepages.ucl.ac.uk/~uctytbu/OERs.html), and [Calgary](https://forallx.openlogicproject.org) versions) + +With these macros, one can typeset natural deduction proofs in Fitch +style, as in the following example: + +![](fitchexample.png) + +``` +\begin{nd} + \hypo {1} {\forall y \neg P(y)} + \open + \hypo {2} {\exists x P(x)} + \open[u] + \hypo {3} {P(u)} + \have {4}{\forall y \neg P(y)} \r{1} + \have {5} {\neg P(u)} \Ae{4} + \have {6} {\bot} \ne{3,5} + \close + \have {6a} {\bot} \Ee{2,3-6} + \close + \have {7} {\neg \exists x P(x)} \ni{2-6a} +\end{nd} +``` + +The output is shown above, and the corresponding LaTeX code below. + +## Changes + +**v0.6, Sept 4, 2023.** Updated the documentation and license (from +GPL to LPPL). The code is essentially unchanged. + +**v0.5, Feb 8, 2005.** The ability to handle multi-line formulas +was added. + +## Download + +The package is available on CTAN as +[`fitch`](https://ctan.org/pkg/fitch). + +The code is [maintained on Github](https://github.com/OpenLogicProject/fitch/). + +## Related packages + +- The [`lplfitch`](https://ctan.org/pkg/lplfitch) packages produces + Fitch-style roofs in the format used in Barwise & Etchemendy's textbook + _Language, Proof, and Logic_. +- The [`natded`](https://ctan.org/pkg/natded) package produces natural + deduction roofs in the style of Jaśkowski, or that of Kalish and + Montague. + +Additional packages for proofs, including Johan Klüwer's, are +available at a [page maintained by Alex Kocurek](https://www.actual.world/latex/) + +## People + +Peter Selinger, Dalhousie University, is the original author. + +Richard Zach, University of Calgary, it the current maintainer. + +## License + +Copyright (C) 2002-2023 Peter Selinger + +This work may be distributed and/or modified under the conditions of +the LaTeX Project Public License, either version 1.3 of this license +or (at your option) any later version. The latest version of this +license is in + + https://www.latex-project.org/lppl.txt + +and version 1.3c or later is part of all distributions of LaTeX +version 2008 or later.
\ No newline at end of file diff --git a/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt b/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt new file mode 100644 index 00000000000..df4af5c4da6 --- /dev/null +++ b/Master/texmf-dist/doc/latex/fitch/fitch.hacker.txt @@ -0,0 +1,314 @@ +This file describes the internals of the macros in fitch.sty. It is +intended for programmers who might want to hack this package. For +information on how to use the package, please see the user guide, +which is provided in the file fitchdoc.tex. + +GENERAL + +Global identifiers defined by this package start with '\nd*'. The only +exceptions are \ndref, \nddim, \ndindent, and the "nd" and "ndresume" +latex environments. + +The macros provided by this package mix TeX and LaTeX primitives. +LaTeX is used for \rule, \settowidth, \addtolength, \hspace... All +macros are assumed to be called in math mode. + +Translation proceeds through several layers of macros. Each layer +consist of macros which expand into macros of the previous layer. Each +layer may have some global state and initialization functions. Only +the topmost layer (layer D) is directly user-accessible. + +REFERENCES + +We start with some macros to facilitate automatic line numbering, and +for referencing of lines by labels. The macros defined here are: +\nd*reset to reset the line number count. \nd*num{x}, to generate the +next line number and store it in reference x; \nd*ref{x} to print the +line number referenced by x, \ndref{xxx} to parse a list of +references, separated by commas, periods, and hyphens, and translate +all references to line numbers. Note: \ndref ignores spaces in its +argument, but puts a space after each comma or period in the +output. Also note: \nd*ref can be useful outside a natded environment, +and thus it has a user accessible name. Most general ``line numbers'' +actually consist of a name (such as ``n'') and a number (such as +``2''), to produce output such as $n+2$. \nd*set{n}{m} is called to +set the letter to n and the number to m. As special cases, if the +second argument is empty, it is not set, and if the first argument is +\relax, it is not set. + +Example for references: + +\nd*reset \nd*num{x}; \nd*num{y}; \nd*numopt{n+1}{z}; \nd*num{zz}; +\nd*ref{y}; \ndref{x, y-zz, z} +will produce: 1; 2; n+1; 3; 2; 1, 2-3, n+1 + +LAYER A + +Layer A provides primitive picture elements which can be combined into +natural deduction derivations. These are: \nd*t to make a topmost +vertical line segment; \nd*v to make a continuation vertical line +segment, \nd*i to produce the indentation for a subproof, \nd*s to +produce the horizontal space between a vertical line and a formula, +\nd*u{x} to underline x with appropriate spacing for a +hypothesis. \nd*f{x} typesets the formula x with the appropriate +vertical spacing. \nd*g{x} is like \nd*i, except it puts a guard in +the space it creates. These elements are spaced so that they are +appropriate as left-aligned array entries. Line numberings and +justifications must be provided manually in this layer. All explicit +spacing information is contained in this layer; higher layers +manipulate only layer A primitives. + +Example of a derivation using layer A syntax: + +\[ +\begin{array}{lll} + 1 & \nd*t\nd*s\nd*f {P\vee Q} \\ + 2 & \nd*v\nd*s\nd*u {\neg Q} \\ + 3 & \nd*v\nd*i\nd*t\nd*s\nd*u {P} \\ + 4 & \nd*v\nd*i\nd*v\nd*s\nd*f {P} & \mbox{by 3} \\ + 5 & \nd*v\nd*i\nd*t\nd*s\nd*u {Q} \\ + 6 & \nd*v\nd*i\nd*v\nd*s\nd*f {\neg Q} & \mbox{by 2} \\ + 7 & \nd*v\nd*i\nd*v\nd*s\nd*f {\bot} & \mbox{by 5, 6} \\ + 8 & \nd*v\nd*i\nd*v\nd*s\nd*f {P} & \mbox{by 7} \\ + 9 & \nd*v\nd*s\nd*f {P} & \mbox{by 1, 3-4, 5-8} \\ +\end{array} +\] + +LISTS + +This is a bit of a hack. We implement linked lists as follows: a list +is either \nd*nil, or \nd*cons{T}{H}, where T is another list, and H +is some arbitrary code. Note that lists grow to the right. The +following macros operate on a list that is stored in a macro \list. + +\nd*push\list{item} pushes the item onto the list +\nd*pop\list{item} pops and discards the last item from the list +\nd*item\list{command} applies command to each element of the list +\nd*modify\list\n{elt} modifies the \n-th element of the +list, if there is such an element. Here \n is a counter. Elements +are counted from the right, starting from 1. + +We use lists of items of the forms \nd*t, \nd*v, \nd*i, and \nd*g{...} +to represent the current indentation level and format (see Layer A, +above). The function \nd*cont computes the indentation for the +following line by replacing all items of the form \nd*t by \nd*v and +\nd*g{...} by \nd*i. + +With the list syntax, a derivation can be expressed like this: + +\[ +\begin{array}{lll} + \gdef\stack{\nd*nil} + \newcount\n + \nd*push\stack{\nd*t} + 1 & \nd*iter\stack\relax\nd*s\nd*u {\neg\exists xP(x)} \\ + \nd*cont\stack + \nd*push\stack{\nd*i} + \nd*push\stack{\nd*t} + \nd*n=2\nd*modify\stack\n{\nd*g{u}} + \nd*push\stack{\nd*i} + \nd*push\stack{\nd*t} + 2 & \nd*iter\stack\relax\nd*s\nd*u {P(u)} \\ + \nd*cont\stack + 3 & \nd*iter\stack\relax\nd*s\nd*f {\exists xP(x)} \\ + \nd*cont\stack + 4 & \nd*iter\stack\relax\nd*s\nd*f {\neg\exists xP(x)} \\ + \nd*cont\stack + 5 & \nd*iter\stack\relax\nd*s\nd*f {\bot} \\ + \nd*cont\stack + \nd*pop\stack + \nd*pop\stack + 6 & \nd*iter\stack\relax\nd*s\nd*f {\neg P(u)} \\ + \nd*cont\stack + \nd*pop\stack + \nd*pop\stack + 7 & \nd*iter\stack\relax\nd*s\nd*f {\forall y\neg P(y)} \\ + \nd*cont\stack +\end{array} +\] + +LAYER B + +Layer B is simply a wrapper around layer A. It provides commands +\nd*beginb, \nd*resumeb, \nd*endb, \nd*openb, \nd*closeb, \nd*guardb, +\nd*hypob, and \nd*haveb which abstract from the layer A +primitives. This includes automatic line numbering, and automatic +indentation. \nd*hypocontb and \nd*havecontb are like \nd*hypob and +\nd*haveb, except that they introduce continuation lines that are +slightly indented and have no line number/label. \nd*beginb and +\nd*endb enclose a natural deduction in layer B syntax. \nd*resumeb is +like \nd*beginb, except that it resumes a deduction in progress (for +instance, after a manual page break). \nd*openb and \nd*closeb open, +respectively close, a subproof. \nd*guardb{n}{g} adds the guard g to +the nth enclosing subderivation (counted from 1 from the +inside). \nd*hypob introduces a hypothesis, and \nd*haveb introduces a +non-hypothesis line in a proof. Line numbering is integrated, but +justifications must still be given manually. Also, proof lines must +still be terminated by '\\'. An idiosyncracy of this layer is that in +a list of several hypotheses, all but the last one must be called with +\nd*haveb, not \nd*hypob, to avoid drawing a horizontal line under +each of them. + +Example of a derivation using layer B syntax. Note that the "line +numbers" are really labels, which will be replaced by consecutive line +numbers in the output. + +\[ + \nd*beginb + \nd*haveb {1}{P\vee Q} \\ + \nd*hypob {2}{\neg Q} \\ + \nd*openb + \nd*hypob {3}{P} \\ + \nd*haveb {4}{P} \mbox{by \ndref{3}} \\ + \nd*closeb + \nd*openb + \nd*hypob {5}{Q} \\ + \nd*haveb {6}{\neg Q} \mbox{by \ndref{2}} \\ + \nd*haveb {6a}{\bot} \mbox{by \ndref{5,6}} \\ + \nd*haveb {6b}{P} \mbox{by \ndref{6a}} \\ + \nd*closeb + \nd*haveb {8}{P} \mbox{by \ndref{1,3-4,5-6b}} \\ + \nd*endb +\] + +Here is another example, using a guard. + +\[ + \nd*beginb + \nd*hypob {1}{\neg\exists xP(x)} \\ + \nd*openb + \nd*guardb {1}{u} + \nd*openb + \nd*hypob {2}{P(u)} \\ + \nd*haveb {3}{\exists xP(x)} \mbox{by \ndref{2}} \\ + \nd*haveb {4}{\neg\exists xP(x)} \mbox{by \ndref{1}} \\ + \nd*haveb {5}{\bot} \mbox{by \ndref{3,4}}\\ + \nd*closeb + \nd*haveb {6}{\neg P(u)} \mbox{by \ndref{2-5}}\\ + \nd*closeb + \nd*haveb {7}{\forall y\neg P(y)} \mbox{by \ndref{2-6}}\\ + \nd*endb +\] + +LAYER C + +Layer C is a wrapper around layer B. It takes care of buffering +information and putting it correctly into an array. Specifically, in +layer C, it is no more necessary to explicitly give '\\', and all +hypotheses are denoted \hypo. Layer C also provides a convenient +syntax for writing justification labels. Further, layer C provides +``multi-line'' commands, thus e.g. \nd*mhypoc{a}{x\\y\\z} is an +abbreviation for \nd*hypoc{a}{x}\nd*hypocontc{y}\nd*hypocontc{z}. In +addition there is a \nd*by command for writing justification labels, +in the style of \nd*by{$\vee$E}{1,2-4,5-6}. + +Commands exported by layer C are: \nd*hypoc, \nd*havec, \nd*hypocontc, +\nd*havecontc, \nd*mhypoc, \nd*mhavec, \nd*mhypocontc, \nd*mhavecontc, +\nd*by, \nd*beginc, \nd*resumec, \nd*endc, \nd*openc, \nd*closec, +\nd*guardc. + +The layer C macros work by storing each line in a data structure +\ppp,\nd*typ,\nd*byt. The line is ejected when the beginning of the +next line is read, and once at the very end. In this way, we can put +in the correct line breaks (whether or not the line carries a +justification), and a hypothesis does not get typeset until we know +whether it is followed by another hypothesis. \nd*sto stores a new +line, \nd*clr clears the current line, \nd*cmd outputs the current +line. + +Example of layer C syntax: + +\[ + \nd*beginc + \nd*hypoc {1}{\neg\exists xP(x)} + \nd*openc + \nd*guardc {1}{u} + \nd*openc + \nd*hypoc {2}{P(u)} + \nd*havec {3}{\exists xP(x)} \nd*by{$\exists$I}{2} + \nd*havec {4}{\neg\exists xP(x)} \nd*by{R}{1} + \nd*havec {5}{\bot} \nd*by{$\neg$E}{3,4} + \nd*closec + \nd*havec {6}{\neg P(u)} \nd*by{$\neg$I}{2-5} + \nd*closec + \nd*havec {7}{\forall y\neg P(y)} \nd*by{$\forall$I}{2-6} + \nd*endc +\] + +LAYER D + +Layer D is the syntax used by the end user. It is implemented as a +wrapper around layer C, providing three additional conveniences: (1) a +latex environment, (2) guard as optional argument to \have, \hypo, or +\open, (3) optional relabeling arguments. The user level commands are +similar to those of layer C: they are called \begin{nd}, \end{nd}, +\open, \close, \hypo, \have, \guard, \by. For convenience, a number +of abbreviations are also provided for writing justifications. For +instance \ie for \by{$\Rightarrow$E} etc. These commands are only +visible inside an nd-environment; thus they do not interfere with the +global name space. There is also an environment ndresume which is like +nd, except that it continues a proof in progress (with continuous +nesting and labeling). + +The macros \nd*hypod, \nd*haved, \nd*opend, \nd*guardd are essentially +the user-level macros, but with all optional argument spelled-out. The +versions without the final "d" allow the optional arguments to be +omitted. + +The functions \nd*optarg and \nd*optargg are used to handle optional +arguments. Usage: \nd*optarg{default}{continuation}xxx - reads an +optional argument, supplies default if necessary, then continues with +continuation. Continuation expects optional argument between +[...]. I.e., \nd*optarg{d}{c}[xxx] => c[xxx], and \nd*optarg{d}{c}x => +c[d]x if x != '['. Behavior is undefined if x is {[...}. \nd*optargg +is similar except it takes two continuations: first one for optional +argument present, second for not present. It takes no default value. + +The function \nd*five{\a} reads five, partly optional arguments of the +shape [][]{}[]{}, then call \a with these arguments. + +Finally, \nd*init puts all the commands which are visible inside an +nd-environment in the current name space. + +Example of a derivation using layer D syntax. As before, the "line +numbers" are really labels, which will be replaced by consecutive line +numbers in the output. + +\[ +\begin{nd} + \hypo{1} {P\vee Q} + \hypo{2} {\neg Q} + \open + \hypo{3a} {P} + \have{3b} {P} \r{3a} + \close + \open + \hypo{4a} {Q} + \have{4b} {\neg Q} \r{2} + \have{4c} {\bot} \ne{4a,4b} + \have{4d} {P} \be{4c} + \close + \have{5} {P} \oe{1,3a-3b,4a-4d} +\end{nd} +\] + +Another example of layer D syntax, using guards and relabelings: + +\[ +\begin{nd} + \hypo {1} {P\vee Q} + \open[u] + \hypo {2} {P} + \have [\vdots] {3} {\vdots} + \have [n][-1] {4} {A\wedge B} + \close + \open + \hypo {5} {Q} + \have [\vdots] {6} {\vdots} + \have [m] {7} {A\wedge B} + \close + \have {8} {A\wedge B} \oe{1,2-(4),5-7} + \have [\vdots] {9} {\vdots} + \have [][100] {10} {A} \ae{8} +\end{nd} +\] diff --git a/Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdf b/Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdf Binary files differnew file mode 100644 index 00000000000..33f61cb99e6 --- /dev/null +++ b/Master/texmf-dist/doc/latex/fitch/fitchdoc-dimen.pdf diff --git a/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf b/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf Binary files differnew file mode 100644 index 00000000000..c0948c9096a --- /dev/null +++ b/Master/texmf-dist/doc/latex/fitch/fitchdoc.pdf diff --git a/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex b/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex new file mode 100644 index 00000000000..1889721dd09 --- /dev/null +++ b/Master/texmf-dist/doc/latex/fitch/fitchdoc.tex @@ -0,0 +1,406 @@ +%% fitchdoc.tex +%% Macros for Fitch-style natural deduction (documentation) +%% Copyright 2002-2023 Peter Selinger +% +% This work may be distributed and/or modified under the +% conditions of the LaTeX Project Public License, either version 1.3 +% of this license or (at your option) any later version. +% The latest version of this license is in +% https://www.latex-project.org/lppl.txt +% and version 1.3c or later is part of all distributions of LaTeX +% version 2008 or later. +% +% This work has the LPPL maintenance status `maintained'. +% +% The Current Maintainer of this work is Richard Zach <rzach@ucalgary.ca> +% +% This work consists of the files fitch.sty and fitchdoc.tex. + +% Original Author: Peter Selinger, Dalhousie University +% Created: Jan 14, 2002 +% Modified: Sep 4, 2023 +% Version: 0.6 +% Copyright: (C) 2002-2023 Peter Selinger +% Filename: fitch.sty +% Documentation: fitchdoc.tex +% https://github.com/OpenLogicProject/fitch/ + +\documentclass{ltxdoc} + +\usepackage{fitch,graphicx,showexpl,fullpage} + +\lstset{% + basicstyle=\ttfamily\small, + commentstyle=\itshape\ttfamily\small, + showspaces=false, + showstringspaces=false, + breaklines=true, + breakautoindent=true, + captionpos=t +} + +\title{\texttt{fitch.sty}: Fitch-style natural deduction macros} + +\author{Peter Selinger\\Dalhousie University\thanks{The current +maintainer of this package is \href{https://richardzach.org}{Richard +Zach}. The package repository is at +\url{https://github.com/OpenLogicProject/fitch/}, where you can also +report any \href{https://github.com/OpenLogicProject/fitch/issues}{issues} with it.}} + +\date{Version 0.6\\ September 4, 2023} + +\begin{document} +\maketitle + +\section{Overview} + +This document describes how to use the {\tt fitch.sty} macros for +typesetting Fitch-style natural deduction derivations. To load the macros, +simply put \verb!\usepackage{fitch}! into the preamble of your +{\LaTeX} file. + +Here is a natural deduction derivation, together with the code that +produced it: + +\begin{LTXexample} +\[ +\begin{nd} + \hypo {1} {P\vee Q} + \hypo {2} {\neg Q} + \open + \hypo {3} {P} + \have {4} {P} \r{3} + \close + \open + \hypo {aa} {Q} + \have {6} {\neg Q} \r{2} + \have {7} {\bot} \ne{aa,6} + \have {8} {P} \be{7} + \close + \have {9} {P} \oe{1,3-4,aa-8} +\end{nd} +\] +\end{LTXexample} + +A derivation consists of \emph{lines}, and each line contains a {\em +line number} and a \emph{formula}. Some lines also carry a {\em +justification}. Moreover, each line is either a \emph{hypothesis} or a +\emph{derived formula}. Generally, derived formulas carry a +justification, whereas hypotheses do not; however, the macros do not +enforce this. + +\DescribeEnv{nd} +Derivations are typeset inside the \verb!nd! environment, which must be +used in math mode. + +\DescribeMacro{\hypo}\DescribeMacro{\have} +The commands \verb!\hypo! and \verb!\have! are used +to typeset one line of the derivation; \verb!\hypo! is used for +hypotheses, and \verb!\have! for derived formulas. Both commands take +a label and a formula as an argument. Note that the labels used to +identify lines in the derivation need not be actual line numbers; for +instance, in the above example, we used the label $aa$ instead of $5$. +In the output, lines are automatically numbered consecutively. Labels +may not contain any punctuation characters or spaces. + +\DescribeMacro{\open}\DescribeMacro{\close} +Subderivations are opened and closed with the commands \verb!\open! and +\verb!\close!. Finally, the following commands are provided for +annotating lines with justifications: + +\medskip +\hfill +\begin{tabular}{@{}ll@{}} + \verb!\r! & reiteration \\ + \verb!\ii! & implication introduction \\ + \verb!\ie! & implication elimination \\ + \verb!\ai! & and introduction \\ + \verb!\ae! & and elimination \\ +\end{tabular} +\hfill +\begin{tabular}{ll} + \verb!\oi! & or introduction \\ + \verb!\oe! & or elimination \\ + \verb!\ni! & not introduction \\ + \verb!\ne! & not elimination \\ + \verb!\be! & bottom elimination \\ +\end{tabular} +\hfill +\begin{tabular}{@{}ll@{}} + \verb!\nne! & double negation elimination \\ + \verb!\Ai! & forall introduction \\ + \verb!\Ae! & forall elimination \\ + \verb!\Ei! & exists introduction \\ + \verb!\Ee! & exists elimination \\ +\end{tabular} +\hfill +\medskip + +Each such command takes a \emph{reference list} as an argument. A +reference list is a string made from labels, commas, and hyphens, for +instance \verb!1,3a-3b,4a-4d!. + +\section{Details} + +\subsection{Guards} + +Some natural deduction derivations with quantifiers use \emph{guards}, as in +the following example: + +\begin{LTXexample} +\[ +\begin{nd} + \hypo {1} {\exists x\forall y.P(x,y)} + \open[v] + \open[u] + \hypo {2} {\forall y.P(u,y)} + \have {3} {P(u,v)} \Ae{2} + \have {4} {\exists x.P(x,v)} \Ei{3} + \close + \have {5} {\exists x.P(x,v)} \Ee{1,2-5} + \close + \have {6} {\forall y\exists x.P(x,y)} \Ai{2-5} +\end{nd} +\] +\end{LTXexample} + +The guards $v$ and $u$ in line 2 were typeset by giving optional +arguments to the \verb!\open! commands of the respective +subderivations. + +\DescribeMacro{\guard} +For most purposes, the above way of specifying guards is sufficient. +However, there is another method, which allows a more flexible +placement of guards: before any line, you can give the command +\verb!\guard{u}! to add a guard $u$ to the top-level subderivation at +that line, or \verb!\guard[n]{u}! to add a guard to the $n$th +enclosing subderivation at that line. Thus, the above example could +have also been typeset by inserting the two commands \verb!\guard{u}! and +\verb!\guard[2]{v}! just after the second \verb!\open! statement. + +% For backward compatibility, there is a third way of specifying guards +% by giving an optional second argument to the \verb!\hypo! and +% \verb!\have! commands. The use of this feature is discouraged. + +\subsection{Generic justifications} + +Non-standard justifications can be created with the \verb!\by! +command. This command takes two arguments: a name and a reference +list. For instance, the command \verb!\by{De Morgan}{lab3,lab4}! might +produce the output ``\mbox{De Morgan, 3, 4}''. Note that the justification +is typeset in text mode. A comma is automatically inserted between the +name and the reference list, unless the reference list is empty. + +\subsection{Label and reference list details} + +Labels may not contain commas, periods, semicolons, hyphens, +parenthesis, or spaces. In a reference list, spaces are ignored (even +within a label!), whereas commas, periods, semicolons, parenthesis, +and hyphens are copied to the output. All other characters are +interpreted as part of a label. Attempting to reference a label which +has not been previously defined by any \verb!\hypo! or \verb!\have! +command produces an error message of the form: + +\begin{verbatim} + ! Package fitch Error: Undefined line reference: lab17. +\end{verbatim} + +\subsection{Referencing line numbers in the text} +\label{subsec-ndref} + +\DescribeMacro{\ndref} +Labels defined in an \verb!nd! environment can be referenced in the +text with the \verb!\ndref! command. This command takes a reference +list as an argument, and produces the corresponding output. However, +it is only possible to reference labels \emph{after} the corresponding +derivation has been typeset. There is currently no convenient way of +defining forward references. Also, if a label is used more than once, +\verb!\ndref! will always refer to the most recent time it was used. + +\subsection{Scope} + +The commands \verb!\hypo!, \verb!\have!, \verb!\open!, \verb!\close!, +\verb!\r!, \verb!\ii!, and so forth are only available inside an +\verb!nd! environment. These commands may have a different meaning +elsewhere in the same document. The only commands provided by the +\verb!fitch.sty! package which are visible outside an \verb!nd! +environment are the command \verb!\ndref! described in +Section~\ref{subsec-ndref}, and the command \verb!\nddim! and the +dimension \verb!\ndindent! described in Section~\ref{subsec-nddim}. + +\subsection{Breaking it across pages}\label{subsec-break} + +\DescribeMacro{\ndresume} +The \verb!nd! environment is derived from the {\LaTeX} \verb!array! +environment, and thus it does not break across pages automatically. +However, if a derivation is too long to fit on a single page, it is +possible to split it manually into physically independent, but +logically consecutive subparts. For this purpose, the \verb!ndresume! +environment is provided to continue a previously interrupted +derivation. Here is an example: + +\begin{LTXexample} +$ +\begin{nd} + \hypo {1} {P\vee Q} + \hypo {2} {\neg Q} + \open + \hypo {3} {P} + \have {4} {P} \r{3} + \close + \open + \hypo {aa} {Q} + \have {6} {\neg Q} \r{2} +\end{nd} +$ + +Derivations can be interrupted and +resumed at any point. + +$ +\begin{ndresume} + \have {7} {\bot} \ne{aa,6} + \have {8} {P} \be{7} + \close + \have {9} {P} \oe{1,3-4,aa-8} +\end{ndresume} +$ +\end{LTXexample} + +\subsection{Custom line numbers} + +One often needs to write derivation schemas, rather than derivations. +This often requires the use of symbolic constants such as $n$, $n+1$, +etc, instead of actual line numbers. The \verb!\have! and \verb!\hypo! +commands have an optional first argument which is a symbolic constant. +For instance, \verb!\have[n]! will cause the current line to be +numbered with the symbolic constant $n$. Subsequent lines are +automatically numbered $n+1$ etc. An initial offset can be given as a +second optional argument, as in \verb!\have[n][-1]!, which will cause +the current line to be numbered $n-1$, the following line $n$, etc. In +an explicit offset is given, the symbolic constant can also be absent: +for instance, the command \verb!\have[][7]! resets the current line +number to $7$. The following example illustrates this behavior: + +\begin{LTXexample} +\[ +\begin{nd} + \hypo {1} {P\vee Q} + \open + \hypo {2} {P} + \have [\vdots] {3} {\vdots} + \have [n][-1] {4} {A\wedge B} + \close + \open + \hypo {5} {Q} + \have [\vdots] {6} {\vdots} + \have [m] {7} {A\wedge B} + \close + \have {8} {A\wedge B} \oe{1,2-(4),5-7} + \have [\vdots] {9} {\vdots} + \have [][100] {10} {A} \ae{8} +\end{nd} +\] +\end{LTXexample} + +Note that in the justification for line $m+1$, parentheses had to be +put around the label $4$. There is currently no way of doing this +automatically. + +{\bf Exercise.} How does one typeset an empty line number? + +{\bf Solution.} Since \verb!\have[]! has a special meaning as explained +above, we need to use \verb!\have[~]! instead. + +\subsection{Continuation lines}\label{subsec-continuation} + +Sometimes one has to typeset a very long formula that does not fit on +a single line. As of version 0.5 of the {\tt fitch.sty} macros, it is +possible to break a formula into several lines using \verb!\\! as a +line separator. Continuation lines are automatically indented, as +shown in the following example. + +\begin{LTXexample} +\[ +\begin{nd} + \hypo{1} {A\wedge B} + \hypo{2} {A\wedge B\rightarrow{} \\ + C\wedge D} + \have{3} {C\wedge D} \ie{1,2} + \have{4} {A\wedge B\wedge{} \\ + C\wedge D} \ai{1,3} +\end{nd} +\] +\end{LTXexample} + +\DescribeMacro{\hypocont} +\DescribeMacro{\havecont} +Alternatively, the \verb!\havecont! and \verb!\hypocont! commands can +be used to specify each continuation line separately, as the following +example illustrates. + +\begin{LTXexample} +\[ +\begin{nd} + \hypo{1} {A\wedge B} + \hypo{2} {A\wedge B\rightarrow{}} + \hypocont {C\wedge D} + \have{3} {C\wedge D} \ie{1,2} + \have{4} {A\wedge B\wedge{}} \ai{1,3} + \havecont {C\wedge D} +\end{nd} +\] +\end{LTXexample} + +This latter style gives slightly more flexibility in the placement of +justifications, since each line and continuation line can have its own +justification and its own guard (via the \verb!\guard! command). It +also allows a derivation to be interrupted between a line and its +continuation, as discussed in Section~\ref{subsec-break}. + +\subsection{Customizing dimensions}\label{subsec-nddim} + +\DescribeMacro{\nddim} +The relative sizes of the various elements of a natural deduction +proof are preset to reasonable values depending on the size of the +currently selected font. However, it will sometimes be necessary to +customize these dimensions. This can be achieved with the +\verb!\nddim! command. The syntax of the command is as follows: +\begin{center} + \cmd{\nddim}\marg{height}\marg{topheight}\marg{depth}\marg{labelsep} + \marg{indent}\marg{hsep}\marg{justsep}\marg{linethickness}, +\end{center} +where each of the eight parameters is a dimension. The meaning of the +first seven parameters is shown in the +following illustrations; \emph{linethickness} is simply the thickness +of the lines. +\[\includegraphics{fitchdoc-dimen}\] +The default dimensions are: +\begin{center} +\verb!\nddim{4.5ex}{3.5ex}{1.5ex}{1em}{1.6em}{.5em}{2.5em}{.2mm}!. +\end{center} +\DescribeMacro{\ndindent} +In addition, the dimension \verb!\ndindent!, controls +the amount of extra indentation used on continuation lines as +discussed in Section~\ref{subsec-continuation}. It can be changed and +is \verb!1ex! by default. + +\subsection{Other comments} + +The goal was to design a flexible package which would not impose any +constraints on the form of derivations, while making typesetting easy. +With this package, it is in fact possible to typeset incomplete, +ill-formed, or invalid derivations. Sometimes it is pedagogically necessary +to do so. + +There are no arbitrary limits on the size or nesting depth of a derivation, +except for the obvious requirement of fitting horizontally on the +printed page. + +\section{Copyright and license} + +This document and the accompanying \verb!fitch.sty! macros +are {\copyright} 2002--2023 by Peter Selinger and distributed under +the terms of the \href{https://www.latex-project.org/lppl/}{LPPL}. + +\end{document} diff --git a/Master/texmf-dist/doc/latex/fitch/fitchexample.png b/Master/texmf-dist/doc/latex/fitch/fitchexample.png Binary files differnew file mode 100644 index 00000000000..d66390786e7 --- /dev/null +++ b/Master/texmf-dist/doc/latex/fitch/fitchexample.png diff --git a/Master/texmf-dist/tex/latex/fitch/fitch.sty b/Master/texmf-dist/tex/latex/fitch/fitch.sty new file mode 100644 index 00000000000..59e06c5a61c --- /dev/null +++ b/Master/texmf-dist/tex/latex/fitch/fitch.sty @@ -0,0 +1,231 @@ +%% fitch.sty +%% Macros for Fitch-style natural deduction +%% Copyright 2002-2023 Peter Selinger +% +% This work may be distributed and/or modified under the +% conditions of the LaTeX Project Public License, either version 1.3 +% of this license or (at your option) any later version. +% The latest version of this license is in +% https://www.latex-project.org/lppl.txt +% and version 1.3c or later is part of all distributions of LaTeX +% version 2008 or later. +% +% This work has the LPPL maintenance status `maintained'. +% +% The Current Maintainer of this work is Richard Zach <rzach@ucalgary.ca> +% +% This work consists of the files fitch.sty and fitchdoc.tex. + +% Original Author: Peter Selinger, Dalhousie University +% Created: Jan 14, 2002 +% Modified: Sep 4, 2023 +% Version: 0.6 +% Copyright: (C) 2002-2005 Peter Selinger +% Filename: fitch.sty +% Documentation: fitchdoc.tex +% https://github.com/OpenLogicProject/fitch/ + +% USAGE EXAMPLE: +% +% The following is a simple example illustrating the usage of this +% package. For detailed instructions and additional functionality, see +% the user guide, which can be found in the file fitchdoc.tex. +% +% \[ +% \begin{nd} +% \hypo{1} {P\vee Q} +% \hypo{2} {\neg Q} +% \open +% \hypo{3a} {P} +% \have{3b} {P} \r{3a} +% \close +% \open +% \hypo{4a} {Q} +% \have{4b} {\neg Q} \r{2} +% \have{4c} {\bot} \ne{4a,4b} +% \have{4d} {P} \be{4c} +% \close +% \have{5} {P} \oe{1,3a-3b,4a-4d} +% \end{nd} +% \] + +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{fitch}[2023-09-04 v0.6 Macros for Fitch-style natural deduction] + +{\chardef\x=\catcode`\* +\catcode`\*=11 +\global\let\nd*astcode\x} +\catcode`\*=11 + +% References + +\newcount\nd*ctr +\def\nd*render{\expandafter\ifx\expandafter\nd*x\nd*base\nd*x\the\nd*ctr\else\nd*base\ifnum\nd*ctr<0\the\nd*ctr\else\ifnum\nd*ctr>0+\the\nd*ctr\fi\fi\fi} +\expandafter\def\csname nd*-\endcsname{} + +\def\nd*num#1{\nd*numo{\nd*render}{#1}\global\advance\nd*ctr1} +\def\nd*numopt#1#2{\nd*numo{$#1$}{#2}} +\def\nd*numo#1#2{\edef\x{#1}\mbox{$\x$}\expandafter\global\expandafter\let\csname nd*-#2\endcsname\x} +\def\nd*ref#1{\expandafter\let\expandafter\x\csname nd*-#1\endcsname\ifx\x\relax% + \PackageWarning{fitch}{Undefined line reference: #1}\mbox{\textbf{??}}\else\mbox{$\x$}\fi} +\def\nd*noop{} +\def\nd*set#1#2{\ifx\relax#1\nd*noop\else\global\def\nd*base{#1}\fi\ifx\relax#2\relax\else\global\nd*ctr=#2\fi} +\def\nd*reset{\nd*set{}{1}} +\def\nd*refa#1{\nd*ref{#1}} +\def\nd*aux#1#2{\ifx#2-\nd*refa{#1}--\def\nd*c{\nd*aux{}}% + \else\ifx#2,\nd*refa{#1}, \def\nd*c{\nd*aux{}}% + \else\ifx#2;\nd*refa{#1}; \def\nd*c{\nd*aux{}}% + \else\ifx#2.\nd*refa{#1}. \def\nd*c{\nd*aux{}}% + \else\ifx#2)\nd*refa{#1})\def\nd*c{\nd*aux{}}% + \else\ifx#2(\nd*refa{#1}(\def\nd*c{\nd*aux{}}% + \else\ifx#2\nd*end\nd*refa{#1}\def\nd*c{}% + \else\def\nd*c{\nd*aux{#1#2}}% + \fi\fi\fi\fi\fi\fi\fi\nd*c} +\def\ndref#1{\nd*aux{}#1\nd*end} + +% Layer A + +% define various dimensions (explained in fitchdoc.tex): +\newlength{\nd*dim} +\newdimen\nd*depthdim +\newdimen\nd*hsep +\newdimen\ndindent +\ndindent=1em +% user command to redefine dimensions +\def\nddim#1#2#3#4#5#6#7#8{\nd*depthdim=#3\relax\nd*hsep=#6\relax% +\def\nd*height{#1}\def\nd*thickness{#8}\def\nd*initheight{#2}% +\def\nd*indent{#5}\def\nd*labelsep{#4}\def\nd*justsep{#7}} +% set initial dimensions +\nddim{4.5ex}{3.5ex}{1.5ex}{1em}{1.6em}{.5em}{2.5em}{.2mm} + +\def\nd*v{\rule[-\nd*depthdim]{\nd*thickness}{\nd*height}} +\def\nd*t{\rule[-\nd*depthdim]{0mm}{\nd*height}\rule[-\nd*depthdim]{\nd*thickness}{\nd*initheight}} +\def\nd*i{\hspace{\nd*indent}} +\def\nd*s{\hspace{\nd*hsep}} +\def\nd*g#1{\nd*f{\makebox[\nd*indent][c]{$#1$}}} +\def\nd*f#1{\raisebox{0pt}[0pt][0pt]{$#1$}} +\def\nd*u#1{\makebox[0pt][l]{\settowidth{\nd*dim}{\nd*f{#1}}% + \addtolength{\nd*dim}{2\nd*hsep}\hspace{-\nd*hsep}\rule[-\nd*depthdim]{\nd*dim}{\nd*thickness}}\nd*f{#1}} + +% Lists + +\def\nd*push#1#2{\expandafter\gdef\expandafter#1\expandafter% + {\expandafter\nd*cons\expandafter{#1}{#2}}} +\def\nd*pop#1{{\def\nd*nil{\gdef#1{\nd*nil}}\def\nd*cons##1##2% + {\gdef#1{##1}}#1}} +\def\nd*iter#1#2{{\def\nd*nil{}\def\nd*cons##1##2{##1#2{##2}}#1}} +\def\nd*modify#1#2#3{{\def\nd*nil{\gdef#1{\nd*nil}}\def\nd*cons##1##2% + {\advance#2-1 ##1\advance#2 1 \ifnum#2=1\nd*push#1{#3}\else% + \nd*push#1{##2}\fi}#1}} + +\def\nd*cont#1{{\def\nd*t{\nd*v}\def\nd*v{\nd*v}\def\nd*g##1{\nd*i}% + \def\nd*i{\nd*i}\def\nd*nil{\gdef#1{\nd*nil}}\def\nd*cons##1##2% + {##1\expandafter\nd*push\expandafter#1\expandafter{##2}}#1}} + +% Layer B + +\newcount\nd*n +\def\nd*beginb{\begingroup\nd*reset\gdef\nd*stack{\nd*nil}\nd*push\nd*stack{\nd*t}% + \begin{array}{l@{\hspace{\nd*labelsep}}l@{\hspace{\nd*justsep}}l}} +\def\nd*resumeb{\begingroup\begin{array}{l@{\hspace{\nd*labelsep}}l@{\hspace{\nd*justsep}}l}} +\def\nd*endb{\end{array}\endgroup} +\def\nd*hypob#1#2{\nd*f{\nd*num{#1}}&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*u{#2}&} +\def\nd*haveb#1#2{\nd*f{\nd*num{#1}}&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*f{#2}&} +\def\nd*havecontb#1#2{&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*f{\hspace{\ndindent}#2}&} +\def\nd*hypocontb#1#2{&\nd*iter\nd*stack\relax\nd*cont\nd*stack\nd*s\nd*u{\hspace{\ndindent}#2}&} + +\def\nd*openb{\nd*push\nd*stack{\nd*i}\nd*push\nd*stack{\nd*t}} +\def\nd*closeb{\nd*pop\nd*stack\nd*pop\nd*stack} +\def\nd*guardb#1#2{\nd*n=#1\multiply\nd*n by 2 \nd*modify\nd*stack\nd*n{\nd*g{#2}}} + +% Layer C + +\def\nd*clr{\gdef\nd*cmd{}\gdef\nd*typ{\relax}} +\def\nd*sto#1#2#3{\gdef\nd*typ{#1}\gdef\nd*byt{}% + \gdef\nd*cmd{\nd*typ{#2}{#3}\nd*byt\\}} +\def\nd*chtyp{\expandafter\ifx\nd*typ\nd*hypocontb\def\nd*typ{\nd*havecontb}\else\def\nd*typ{\nd*haveb}\fi} +\def\nd*hypoc#1#2{\nd*chtyp\nd*cmd\nd*sto{\nd*hypob}{#1}{#2}} +\def\nd*havec#1#2{\nd*cmd\nd*sto{\nd*haveb}{#1}{#2}} +\def\nd*hypocontc#1{\nd*chtyp\nd*cmd\nd*sto{\nd*hypocontb}{}{#1}} +\def\nd*havecontc#1{\nd*cmd\nd*sto{\nd*havecontb}{}{#1}} +\def\nd*by#1#2{\ifx\nd*x#2\nd*x\gdef\nd*byt{\mbox{#1}}\else\gdef\nd*byt{\mbox{#1, \ndref{#2}}}\fi} + +% multi-line macros +\def\nd*mhypoc#1#2{\nd*mhypocA{#1}#2\\\nd*stop\\} +\def\nd*mhypocA#1#2\\{\nd*hypoc{#1}{#2}\nd*mhypocB} +\def\nd*mhypocB#1\\{\ifx\nd*stop#1\else\nd*hypocontc{#1}\expandafter\nd*mhypocB\fi} +\def\nd*mhavec#1#2{\nd*mhavecA{#1}#2\\\nd*stop\\} +\def\nd*mhavecA#1#2\\{\nd*havec{#1}{#2}\nd*mhavecB} +\def\nd*mhavecB#1\\{\ifx\nd*stop#1\else\nd*havecontc{#1}\expandafter\nd*mhavecB\fi} +\def\nd*mhypocontc#1{\nd*mhypocB#1\\\nd*stop\\} +\def\nd*mhavecontc#1{\nd*mhavecB#1\\\nd*stop\\} + +\def\nd*beginc{\nd*beginb\nd*clr} +\def\nd*resumec{\nd*resumeb\nd*clr} +\def\nd*endc{\nd*cmd\nd*endb} +\def\nd*openc{\nd*cmd\nd*clr\nd*openb} +\def\nd*closec{\nd*cmd\nd*clr\nd*closeb} +\let\nd*guardc\nd*guardb + +% Layer D + +% macros with optional arguments spelled-out +\def\nd*hypod[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd*guardb{1}{#4}\fi\nd*mhypoc{#3}{#5}\nd*set{#1}{#2}} +\def\nd*haved[#1][#2]#3[#4]#5{\ifx\relax#4\relax\else\nd*guardb{1}{#4}\fi\nd*mhavec{#3}{#5}\nd*set{#1}{#2}} +\def\nd*havecont#1{\nd*mhavecontc{#1}} +\def\nd*hypocont#1{\nd*mhypocontc{#1}} +\def\nd*base{undefined} +\def\nd*opend[#1]#2{\nd*cmd\nd*clr\nd*openb\nd*guard{#1}#2} +\def\nd*close{\nd*cmd\nd*clr\nd*closeb} +\def\nd*guardd[#1]#2{\nd*guardb{#1}{#2}} + +% Handling of optional arguments. + +\def\nd*optarg#1#2#3{\ifx[#3\def\nd*c{#2#3}\else\def\nd*c{#2[#1]{#3}}\fi\nd*c} +\def\nd*optargg#1#2#3{\ifx[#3\def\nd*c{#1#3}\else\def\nd*c{#2{#3}}\fi\nd*c} + +\def\nd*five#1{\nd*optargg{\nd*four{#1}}{\nd*two{#1}}} +\def\nd*four#1[#2]{\nd*optarg{0}{\nd*three{#1}[#2]}} +\def\nd*three#1[#2][#3]#4{\nd*optarg{}{#1[#2][#3]{#4}}} +\def\nd*two#1{\nd*three{#1}[\relax][]} + +\def\nd*have{\nd*five{\nd*haved}} +\def\nd*hypo{\nd*five{\nd*hypod}} +\def\nd*open{\nd*optarg{}{\nd*opend}} +\def\nd*guard{\nd*optarg{1}{\nd*guardd}} + +\def\nd*init{% + \let\open\nd*open% + \let\close\nd*close% + \let\hypo\nd*hypo% + \let\have\nd*have% + \let\hypocont\nd*hypocont% + \let\havecont\nd*havecont% + \let\by\nd*by% + \let\guard\nd*guard% + \def\ii{\by{$\Rightarrow$I}}% + \def\ie{\by{$\Rightarrow$E}}% + \def\Ai{\by{$\forall$I}}% + \def\Ae{\by{$\forall$E}}% + \def\Ei{\by{$\exists$I}}% + \def\Ee{\by{$\exists$E}}% + \def\ai{\by{$\wedge$I}}% + \def\ae{\by{$\wedge$E}}% + \def\ai{\by{$\wedge$I}}% + \def\ae{\by{$\wedge$E}}% + \def\oi{\by{$\vee$I}}% + \def\oe{\by{$\vee$E}}% + \def\ni{\by{$\neg$I}}% + \def\ne{\by{$\neg$E}}% + \def\be{\by{$\bot$E}}% + \def\nne{\by{$\neg\neg$E}}% + \def\r{\by{R}}% +} + +\newenvironment{nd}{\begingroup\nd*init\nd*beginc}{\nd*endc\endgroup} +\newenvironment{ndresume}{\begingroup\nd*init\nd*resumec}{\nd*endc\endgroup} + +\catcode`\*=\nd*astcode + +% End of file fitch.sty + diff --git a/Master/tlpkg/bin/tlpkg-ctan-check b/Master/tlpkg/bin/tlpkg-ctan-check index c94dc033f65..22eaa225b01 100755 --- a/Master/tlpkg/bin/tlpkg-ctan-check +++ b/Master/tlpkg/bin/tlpkg-ctan-check @@ -337,7 +337,7 @@ my @TLP_working = qw( fig4latex figbas figbib figchild figflow figput figsize filecontents filecontentsdef filedate filehook fileinfo filemod findhyph fink finstrut fira firamath firamath-otf - first-latex-doc firstaid fistrum fitbox fithesis + first-latex-doc firstaid fistrum fitbox fitch fithesis fix2col fixcmex fixdif fixfoot fixjfm fixlatvian fixltxhyph fixmath fixme fixmetodonotes fixpdfmag fiziko fjodor diff --git a/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc b/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc index 78aac554a72..aa79e5b2693 100644 --- a/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc +++ b/Master/tlpkg/tlpsrc/collection-mathscience.tlpsrc @@ -94,6 +94,7 @@ depend extarrows depend extpfeil depend faktor depend fascicules +depend fitch depend fixdif depend fixmath depend fnspe diff --git a/Master/tlpkg/tlpsrc/fitch.tlpsrc b/Master/tlpkg/tlpsrc/fitch.tlpsrc new file mode 100644 index 00000000000..e69de29bb2d --- /dev/null +++ b/Master/tlpkg/tlpsrc/fitch.tlpsrc |