src/HOL/Quickcheck_Narrowing.thy
changeset 43341 acdac535c7fa
parent 43317 f9283eb3a4bf
child 43356 2dee03f192b7
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 14:04:34 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 14:04:38 2011 +0200
@@ -26,7 +26,7 @@
 
 code_reserved Haskell_Quickcheck Typerep
 
-subsubsection {* Type @{text "code_int"} for Haskell_Quickcheck's Int type *}
+subsubsection {* Type @{text "code_int"} for Haskell Quickcheck's Int type *}
 
 typedef (open) code_int = "UNIV \<Colon> int set"
   morphisms int_of of_int by rule
@@ -218,7 +218,7 @@
 datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
 datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
 
-subsubsection {* From narrowing's deep representation of terms to Code_Evaluation's terms *}
+subsubsection {* From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms *}
 
 class partial_term_of = typerep +
   fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term"