doc-src/Functions/Thy/Functions.thy

   subgoal. Usually this needs injectivity of the constructors, which
   is used automatically by @{text "auto"}.
 *}
 
 by auto
+termination by (relation "{}") simp
 
 
 subsection {* Non-constructor patterns *}
 
 text {*

 function check :: "string \<Rightarrow> bool"
 where
   "check (''good'') = True"
 | "s \<noteq> ''good'' \<Longrightarrow> check s = False"
 by auto
+termination by (relation "{}") simp
 
 
 section {* Partiality *}
 
 text {*