# HG changeset patch # User bulwahn # Date 1300102450 -3600 # Node ID 13904699c85981f7ef5413550baf7e2ac86ad013 # Parent d8c3b26b3da4118bf0e4a314e5366d527241de34 tuned subsubsection names in Quickcheck_Narrowing diff -r d8c3b26b3da4 -r 13904699c859 src/HOL/Library/Quickcheck_Narrowing.thy --- a/src/HOL/Library/Quickcheck_Narrowing.thy Mon Mar 14 12:34:10 2011 +0100 +++ b/src/HOL/Library/Quickcheck_Narrowing.thy Mon Mar 14 12:34:10 2011 +0100 @@ -20,7 +20,7 @@ code_reserved Haskell Typerep -subsubsection {* Type @{text code_int} for Haskell's Int type *} +subsubsection {* Type @{text "code_int"} for Haskell's Int type *} typedef (open) code_int = "UNIV \ int set" morphisms int_of of_int by rule @@ -95,7 +95,7 @@ datatype 'a cons = C type "(term list => 'a) list" -subsubsection {* auxilary functions for Narrowing *} +subsubsection {* Auxilary functions for Narrowing *} consts nth :: "'a list => code_int => 'a"