diff -r 79f41fbdf74a -r ef8d840f39fb src/Doc/Classes/Classes.thy --- a/src/Doc/Classes/Classes.thy Sat Apr 09 20:38:08 2016 +0200 +++ b/src/Doc/Classes/Classes.thy Sat Apr 09 21:42:42 2016 +0200 @@ -146,7 +146,7 @@ @{command definition}). The concluding @{command instance} opens a proof that the given parameters actually conform to the class specification. Note that the first proof step is the @{method - default} method, which for such instance proofs maps to the @{method + standard} method, which for such instance proofs maps to the @{method intro_classes} method. This reduces an instance judgement to the relevant primitive proof goals; typically it is the first method applied in an instantiation proof.