Pour utiliser la logique de Hoare, nous devons charger
les fichiers Hoare.thy et Hoare.ML en
tapant:
use_thy "/usr/local/Isabelle/src/HOL/Hoare/Hoare";
Cette théorie est munie de la tactique hoare_tac
qui consiste à utiliser les règles de déduction de
la logique
de Hoare. Après avoir utilisée cette tactique, il ne
reste
que des sous-buts de la logique des prédicats du premier ordre.