# HG changeset patch
# User haftmann
# Date 1291382544 -3600
# Node ID 580b1a30994c1536e0e160e2f9df5d2544b07cbb
# Parent  500171e7aa59099e3588a45dc67e7f4ffd30b79d
explicit type constraint;
streamlined notation

diff -r 500171e7aa59 -r 580b1a30994c src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Fri Dec 03 10:17:55 2010 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Dec 03 14:22:24 2010 +0100
@@ -17,7 +17,7 @@
 definition
   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
 where
-  [simp]: "list_eq xs ys \<longleftrightarrow> set xs = set ys"
+  [simp]: "xs \<approx> ys \<longleftrightarrow> set xs = set ys"
 
 lemma list_eq_reflp:
   "reflp list_eq"
@@ -1047,14 +1047,14 @@
   and a proof of equivalence *}
 
 inductive
-  list_eq2 ("_ \<approx>2 _")
+  list_eq2 :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>2 _")
 where
   "(a # b # xs) \<approx>2 (b # a # xs)"
 | "[] \<approx>2 []"
-| "xs \<approx>2 ys \<Longrightarrow>  ys \<approx>2 xs"
+| "xs \<approx>2 ys \<Longrightarrow> ys \<approx>2 xs"
 | "(a # a # xs) \<approx>2 (a # xs)"
-| "xs \<approx>2 ys \<Longrightarrow>  (a # xs) \<approx>2 (a # ys)"
-| "\<lbrakk>xs1 \<approx>2 xs2;  xs2 \<approx>2 xs3\<rbrakk> \<Longrightarrow> xs1 \<approx>2 xs3"
+| "xs \<approx>2 ys \<Longrightarrow> (a # xs) \<approx>2 (a # ys)"
+| "xs1 \<approx>2 xs2 \<Longrightarrow> xs2 \<approx>2 xs3 \<Longrightarrow> xs1 \<approx>2 xs3"
 
 lemma list_eq2_refl:
   shows "xs \<approx>2 xs"