Lines Matching defs:meta
13 the meta-logic.
34 \subsection{Deriving a rule using tactics and meta-level assumptions}
44 formulae{} (they do not involve the meta-connectives $\Forall$ or
47 \item If one or more premises involves the meta-connectives $\Forall$ or
50 These meta-level assumptions are also recorded internally, allowing
56 theorems are subject to meta-level assumptions, so we make them visible by by setting the
80 Look at the minor premise, recalling that meta-level assumptions are
125 Definitions are expressed as meta-level equalities. Let us define negation
132 \index{meta-rewriting}%
133 Isabelle permits {\bf meta-level rewriting} using definitions such as
150 Isabelle provides tactics and meta-rules for rewriting, and a version of
158 This requires proving the following meta-formulae:
165 Again, the rule's premises involve a meta-connective, and \texttt{Goal}
283 defs {\it meta-logical definitions}
308 \thydx{Pure} contains nothing but Isabelle's meta-logic. The variant
727 and~$\neg$, we take advantage of the meta-logic;\footnote
751 function-valued expressions. We again take advantage of the meta-logic,