Isabelle/HOL Support Wiki

This is an old revision of the document!

Attribute Examples

This page contains usage examples for attributes (or directives).

of

where

THEN

OF

Consider rule subst:

$\quad [|\ ?s = ?t; ?P ?s\ |]\quad \Longrightarrow\quad ?P ?t$

Note that you can use this rule only to substitute from left to right, not the reverse. Using OF together with theorem sym ( $?s = ?t\ \Longrightarrow\ ?t = ?s$ ), i.e.

  subst [OF sym]

yields

$\quad [|\ ?t = ?s; ?P ?s\ |]\quad \Longrightarrow\quad ?P ?t$

which allows substitutions from right to left.

Isabelle/HOL Support Wiki

Table of Contents

Attribute Examples

of

where

THEN

OF

simplified

rotated

symmetric

Isabelle/HOL Support Wiki

User Tools

Site Tools

Table of Contents

Attribute Examples

of

where

THEN

OF

simplified

rotated

symmetric

Page Tools