src/HOL/MicroJava/J/Example.thy
changeset 24207 402d629925ed
parent 24074 40f414b87655
child 24783 5a3e336a2e37