# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260316486 -3600
# Node ID 5ededdde9e9f30d668a8d84de8de18b339296349
# Parent  02fd9de9d45e2ac67390b006ff4c6adad97b7633
tuned code

diff -r 02fd9de9d45e -r 5ededdde9e9f Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Wed Dec 09 00:03:18 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 00:54:46 2009 +0100
@@ -142,7 +142,6 @@
 (* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
 
-
 declare [[map "fun" = (fun_map, fun_rel)]]
 
 (* Throws now an exception:              *)
@@ -212,8 +211,6 @@
 
 section {* Infrastructure about id *}
 
-print_attributes
-
 (* TODO: think where should this be *)
 lemma prod_fun_id: "prod_fun id id \<equiv> id"
   by (rule eq_reflection) (simp add: prod_fun_def)
@@ -375,8 +372,7 @@
        let
          val subtrm = apply_subt (regularize_trm lthy) t t'
        in
-         if ty = ty'
-         then Const (@{const_name "All"}, ty) $ subtrm
+         if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
          else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
@@ -384,8 +380,7 @@
        let
          val subtrm = apply_subt (regularize_trm lthy) t t'
        in
-         if ty = ty'
-         then Const (@{const_name "Ex"}, ty) $ subtrm
+         if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
          else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
@@ -401,8 +396,7 @@
          val rel_ty = (fastype_of rel) handle TERM _ => raise exc 
          val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') 
        in 
-         if rel' = rel
-         then rtrm else raise exc
+         if rel' = rel then rtrm else raise exc
        end  
   | (_, Const (s, _)) =>
        let 
@@ -418,9 +412,7 @@
              val thy = ProofContext.theory_of lthy
              val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) 
            in 
-             if matches_term (rtrm, rtrm')
-             then rtrm
-             else raise exc2
+             if matches_term (rtrm, rtrm') then rtrm else raise exc2
            end
        end 
 
@@ -443,7 +435,6 @@
 
 ML {*
 fun equiv_tac ctxt =
-  (K (print_tac "equiv tac")) THEN'
   REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
 
 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
@@ -719,8 +710,7 @@
   and   QT_ex:  "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
   and   QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE  (P x))"
   and   QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
-apply(simp_all add: QUOT_TRUE_def ext)
-done
+by (simp_all add: QUOT_TRUE_def ext)
 
 lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"
 by (simp add: QUOT_TRUE_def)
@@ -1047,12 +1037,6 @@
 thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps 
 (* 4. Test for refl *)
 
-thm fun_map.simps
-
-ML {* Conv.abs_conv; term_of *}
-
-thm fun_map.simps[THEN eq_reflection]
-
 ML {*
 fun fun_map_conv xs ctxt ctrm =
   case (term_of ctrm) of
@@ -1064,9 +1048,7 @@
     | _ $ _ => Conv.comb_conv (fun_map_conv xs ctxt) ctrm
     | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
     | _ => Conv.all_conv ctrm
-*}
 
-ML {*
 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
 *}