src/HOL/List.thy
changeset 51314 eac4bb5adbf9
parent 51272 9c8d63b4b6be
child 51315 536a5603a138
     1.1 --- a/src/HOL/List.thy	Thu Feb 28 16:38:17 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Thu Feb 28 16:54:52 2013 +0100
     1.3 @@ -514,11 +514,6 @@
     1.4      Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
     1.5    | _ => raise CTERM ("Collect_conv", [ct]))
     1.6  
     1.7 -fun Trueprop_conv cv ct =
     1.8 -  (case Thm.term_of ct of
     1.9 -    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
    1.10 -  | _ => raise CTERM ("Trueprop_conv", [ct]))
    1.11 -
    1.12  fun eq_conv cv1 cv2 ct =
    1.13    (case Thm.term_of ct of
    1.14      Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv1) cv2 ct
    1.15 @@ -536,7 +531,7 @@
    1.16      (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
    1.17  
    1.18  fun right_hand_set_comprehension_conv conv ctxt =
    1.19 -  Trueprop_conv (eq_conv Conv.all_conv
    1.20 +  HOLogic.Trueprop_conv (eq_conv Conv.all_conv
    1.21      (Collect_conv (all_exists_conv conv o #2) ctxt))
    1.22  
    1.23  
    1.24 @@ -628,7 +623,7 @@
    1.25                          Conv.all_conv)
    1.26                          then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))
    1.27                          then_conv conjunct_assoc_conv)) context
    1.28 -                    then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
    1.29 +                    then_conv (HOLogic.Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
    1.30                        Conv.repeat_conv
    1.31                          (all_but_last_exists_conv
    1.32                            (K (rewr_conv'
    1.33 @@ -644,7 +639,7 @@
    1.34                            (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
    1.35                          Conv.all_conv then_conv
    1.36                          (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
    1.37 -                      Trueprop_conv
    1.38 +                      HOLogic.Trueprop_conv
    1.39                          (eq_conv Conv.all_conv
    1.40                            (Collect_conv (fn (_, ctxt) =>
    1.41                              Conv.repeat_conv