src/Doc/Tutorial/Inductive/Star.thy
changeset 81303 cee03fbcec0d
parent 80983 2cc651d3ce8e