# HG changeset patch
# User huffman
# Date 1315959919 25200
# Node ID 14f7da460ce87cd04ba53e3f73c456012ba58ecd
# Parent  58eef4843641234fb6b36b22a53590f5ca3cd627
tuned proofs

diff -r 58eef4843641 -r 14f7da460ce8 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Tue Sep 13 17:07:33 2011 -0700
+++ b/src/HOL/Record.thy	Tue Sep 13 17:25:19 2011 -0700
@@ -55,9 +55,9 @@
   constant K.
 
   If we prove the access/update theorem on this type with the
-  analagous steps to the tuple tree, we consume @{text "O(log(n)^2)"}
+  analogous steps to the tuple tree, we consume @{text "O(log(n)^2)"}
   time as the intermediate terms are @{text "O(log(n))"} in size and
-  the types needed have size bounded by K.  To enable this analagous
+  the types needed have size bounded by K.  To enable this analogous
   traversal, we define the functions seen below: @{text
   "iso_tuple_fst"}, @{text "iso_tuple_snd"}, @{text "iso_tuple_fst_update"}
   and @{text "iso_tuple_snd_update"}. These functions generalise tuple
@@ -229,61 +229,62 @@
     (f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g =
       j o (f o iso_tuple_fst isom)"
   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps
-    intro!: ext elim!: o_eq_elim)
+    fun_eq_iff)
 
 lemma iso_tuple_access_update_snd_snd:
   "f o h g = j o f \<Longrightarrow>
     (f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g =
       j o (f o iso_tuple_snd isom)"
   by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps
-    intro!: ext elim!: o_eq_elim)
+    fun_eq_iff)
 
 lemma iso_tuple_access_update_fst_snd:
   "(f o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g =
     id o (f o iso_tuple_fst isom)"
   by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps
-    intro!: ext elim!: o_eq_elim)
+    fun_eq_iff)
 
 lemma iso_tuple_access_update_snd_fst:
   "(f o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g =
     id o (f o iso_tuple_snd isom)"
   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps
-    intro!: ext elim!: o_eq_elim)
+    fun_eq_iff)
 
 lemma iso_tuple_update_swap_fst_fst:
   "h f o j g = j g o h f \<Longrightarrow>
     (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g =
       (iso_tuple_fst_update isom o j) g o (iso_tuple_fst_update isom o h) f"
-  by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext)
+  by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff)
 
 lemma iso_tuple_update_swap_snd_snd:
   "h f o j g = j g o h f \<Longrightarrow>
     (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g =
       (iso_tuple_snd_update isom o j) g o (iso_tuple_snd_update isom o h) f"
-  by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext)
+  by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff)
 
 lemma iso_tuple_update_swap_fst_snd:
   "(iso_tuple_snd_update isom o h) f o (iso_tuple_fst_update isom o j) g =
     (iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o h) f"
   by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def
-    simps intro!: ext)
+    simps fun_eq_iff)
 
 lemma iso_tuple_update_swap_snd_fst:
   "(iso_tuple_fst_update isom o h) f o (iso_tuple_snd_update isom o j) g =
     (iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o h) f"
-  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps intro!: ext)
+  by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps
+    fun_eq_iff)
 
 lemma iso_tuple_update_compose_fst_fst:
   "h f o j g = k (f o g) \<Longrightarrow>
     (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g =
       (iso_tuple_fst_update isom o k) (f o g)"
-  by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext)
+  by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff)
 
 lemma iso_tuple_update_compose_snd_snd:
   "h f o j g = k (f o g) \<Longrightarrow>
     (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g =
       (iso_tuple_snd_update isom o k) (f o g)"
-  by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext)
+  by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff)
 
 lemma iso_tuple_surjective_proof_assist_step:
   "iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom o f) \<Longrightarrow>