Induct_word : tactic
STRUCTURE
wordsLib
SYNOPSIS
Initiate an induction on the value of a word.
DESCRIPTION
The tactic Induct_word makes use of the tactic bossLib.recInduct wordsTheory.WORD_INDUCT.
EXAMPLE
Given the goal 
?- !w:word8. P w
one can apply Induct_word to begin a proof by induction. 
- e Induct_word
This results in the base and step cases of the induction as new goals. 
?- P 0w

[SUC n < 256, P (n2w n)] ?- P (n2w (SUC n))
SEEALSO
recInduct
HOL  Trindemossen-1