--- a/src/HOL/Eisbach/Tests.thy Mon May 30 16:11:53 2016 +1000
+++ b/src/HOL/Eisbach/Tests.thy Tue May 31 11:45:34 2016 +1000
@@ -591,4 +591,17 @@
end
+subsection \<open>Mutual recursion via higher-order methods\<close>
+
+experiment begin
+
+method inner_method methods passed_method = (rule conjI; passed_method)
+
+method outer_method = (inner_method \<open>outer_method\<close> | assumption)
+
+lemma "Q \<Longrightarrow> R \<Longrightarrow> P \<Longrightarrow> (Q \<and> R) \<and> P"
+ by outer_method
+
end
+
+end