equal
deleted
inserted
replaced
1145 shows "P x1 x2" |
1145 shows "P x1 x2" |
1146 using assms |
1146 using assms |
1147 by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]]) |
1147 by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]]) |
1148 |
1148 |
1149 ML \<open> |
1149 ML \<open> |
1150 fun dest_fsetT (Type (\<^type_name>\<open>fset\<close>, [T])) = T |
1150 fun dest_fsetT \<^Type>\<open>fset T\<close> = T |
1151 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
1151 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
1152 \<close> |
1152 \<close> |
1153 |
1153 |
1154 no_notation |
1154 no_notation |
1155 list_eq (infix "\<approx>" 50) and |
1155 list_eq (infix "\<approx>" 50) and |