--- a/src/HOL/List.thy Mon Jan 23 15:23:02 2012 +0100
+++ b/src/HOL/List.thy Mon Jan 23 17:29:19 2012 +0100
@@ -5010,8 +5010,8 @@
subsubsection {* Lifting Relations to Lists: all elements *}
inductive_set
- listrel :: "('a * 'a)set => ('a list * 'a list)set"
- for r :: "('a * 'a)set"
+ listrel :: "('a \<times> 'b) set \<Rightarrow> ('a list \<times> 'b list) set"
+ for r :: "('a \<times> 'b) set"
where
Nil: "([],[]) \<in> listrel r"
| Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
--- a/src/HOL/Nominal/Examples/Standardization.thy Mon Jan 23 15:23:02 2012 +0100
+++ b/src/HOL/Nominal/Examples/Standardization.thy Mon Jan 23 17:29:19 2012 +0100
@@ -424,6 +424,7 @@
declare listrel_mono [mono_set]
lemma listrelp_eqvt [eqvt]:
+ fixes f :: "'a::pt_name \<Rightarrow> 'b::pt_name \<Rightarrow> bool"
assumes xy: "listrelp f (x::'a::pt_name list) y"
shows "listrelp ((pi::name prm) \<bullet> f) (pi \<bullet> x) (pi \<bullet> y)" using xy
by induct (simp_all add: listrelp.intros perm_app [symmetric])