src/Pure/Isar/object_logic.ML
changeset 19261 9f8e56d1dbf6
parent 18939 18e2a2676d80
child 20912 380663e636a8
equal deleted inserted replaced
19260:a3d3a4b75c71 19261:9f8e56d1dbf6
    12   val judgment_name: theory -> string
    12   val judgment_name: theory -> string
    13   val is_judgment: theory -> term -> bool
    13   val is_judgment: theory -> term -> bool
    14   val drop_judgment: theory -> term -> term
    14   val drop_judgment: theory -> term -> term
    15   val fixed_judgment: theory -> string -> term
    15   val fixed_judgment: theory -> string -> term
    16   val ensure_propT: theory -> term -> term
    16   val ensure_propT: theory -> term -> term
       
    17   val is_elim: thm -> bool
    17   val declare_atomize: attribute
    18   val declare_atomize: attribute
    18   val declare_rulify: attribute
    19   val declare_rulify: attribute
    19   val atomize_term: theory -> term -> term
    20   val atomize_term: theory -> term -> term
    20   val atomize_cterm: cterm -> thm
    21   val atomize_cterm: cterm -> thm
    21   val atomize_thm: thm -> thm
    22   val atomize_thm: thm -> thm
   113 fun ensure_propT thy t =
   114 fun ensure_propT thy t =
   114   let val T = Term.fastype_of t
   115   let val T = Term.fastype_of t
   115   in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
   116   in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
   116 
   117 
   117 
   118 
       
   119 (* elimination rules *)
       
   120 
       
   121 fun is_elim rule =
       
   122   let
       
   123     val thy = Thm.theory_of_thm rule;
       
   124     val concl = Thm.concl_of rule;
       
   125   in
       
   126     Term.is_Var (drop_judgment thy concl) andalso
       
   127       exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
       
   128   end;
       
   129 
       
   130 
   118 
   131 
   119 (** treatment of meta-level connectives **)
   132 (** treatment of meta-level connectives **)
   120 
   133 
   121 (* maintain rules *)
   134 (* maintain rules *)
   122 
   135