src/Pure/Isar/local_defs.ML
changeset 20021 815393c02db9
parent 19897 fe661eb3b0e7
child 20049 f48c4a3a34bc
equal deleted inserted replaced
20020:9e7d3d06c643 20021:815393c02db9
    54   in map Logic.mk_equals (lhss ~~ rhss) end;
    54   in map Logic.mk_equals (lhss ~~ rhss) end;
    55 
    55 
    56 
    56 
    57 (* export defs *)
    57 (* export defs *)
    58 
    58 
    59 fun head_of_def cprop =
    59 val head_of_def =
    60   Term.head_of (#1 (Logic.dest_equals (Term.strip_all_body (Thm.term_of cprop))))
    60   #1 o Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body o Thm.term_of;
    61   |> Thm.cterm_of (Thm.theory_of_cterm cprop);
    61 
    62 
    62 
    63 (*
    63 (*
    64   [x, x == t]
    64   [x, x == t]
    65        :
    65        :
    66       B x
    66       B x
    68       B t
    68       B t
    69 *)
    69 *)
    70 fun def_export _ cprops thm =
    70 fun def_export _ cprops thm =
    71   thm
    71   thm
    72   |> Drule.implies_intr_list cprops
    72   |> Drule.implies_intr_list cprops
    73   |> Drule.forall_intr_list (map head_of_def cprops)
    73   |> Drule.generalize ([], map head_of_def cprops)
    74   |> Drule.forall_elim_vars 0
       
    75   |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1;
    74   |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1;
    76 
    75 
    77 
    76 
    78 (* add defs *)
    77 (* add defs *)
    79 
    78