author haftmann Mon Sep 05 22:02:32 2011 +0200 (2011-09-05) changeset 44833 9c6bd6204143 parent 44720 f3a8c19708c8 child 44834 242348d1b6d3
tuned
```     1.1 --- a/src/HOL/Nominal/Nominal.thy	Mon Sep 05 14:42:31 2011 +0200
1.2 +++ b/src/HOL/Nominal/Nominal.thy	Mon Sep 05 22:02:32 2011 +0200
1.3 @@ -51,16 +51,16 @@
1.4  begin
1.5
1.6  definition
1.7 -  perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
1.8 +  "perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))"
1.9
1.10  definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
1.11 -  perm_bool_def: "perm_bool pi b = b"
1.12 +  "perm_bool pi b = b"
1.13
1.14  primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit"  where
1.15    "perm_unit pi () = ()"
1.16
1.17  primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where
1.18 -  "perm_prod pi (x,y) = (pi\<bullet>x,pi\<bullet>y)"
1.19 +  "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)"
1.20
1.21  primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where
1.22    nil_eqvt:  "perm_list pi []     = []"
1.23 @@ -71,13 +71,13 @@
1.24  | none_eqvt:  "perm_option pi None     = None"
1.25
1.26  definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where
1.27 -  perm_char_def: "perm_char pi c = c"
1.28 +  "perm_char pi c = c"
1.29
1.30  definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where
1.31 -  perm_nat_def: "perm_nat pi i = i"
1.32 +  "perm_nat pi i = i"
1.33
1.34  definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where
1.35 -  perm_int_def: "perm_int pi i = i"
1.36 +  "perm_int pi i = i"
1.37
1.38  primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where
1.39    nsome_eqvt:  "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
1.40 @@ -962,7 +962,7 @@
1.41    fixes pi::"'y prm"
1.42    and   x ::"'x set"
1.43    assumes dj: "disjoint TYPE('x) TYPE('y)"
1.44 -  shows "(pi\<bullet>x)=x"
1.45 +  shows "pi\<bullet>x=x"
1.46    using dj by (simp_all add: perm_fun_def disjoint_def perm_bool)
1.47
1.48  lemma dj_perm_perm_forget:
1.49 @@ -1028,7 +1028,7 @@
1.50  qed
1.51
1.52  lemma pt_unit_inst:
1.53 -  shows  "pt TYPE(unit) TYPE('x)"
1.54 +  shows "pt TYPE(unit) TYPE('x)"
1.55    by (simp add: pt_def)
1.56
1.57  lemma pt_prod_inst:
```