src/ZF/Tools/typechk.ML
changeset 12202 af10de5ec7cc
parent 12189 4729bbf86626
child 12311 ce5f9e61c037
equal deleted inserted replaced
12201:7198f403a2f9 12202:af10de5ec7cc
    18   val print_tc: tcset -> unit
    18   val print_tc: tcset -> unit
    19   val print_tcset: theory -> unit
    19   val print_tcset: theory -> unit
    20   val tcset_ref_of: theory -> tcset ref
    20   val tcset_ref_of: theory -> tcset ref
    21   val tcset_of: theory -> tcset
    21   val tcset_of: theory -> tcset
    22   val tcset: unit -> tcset
    22   val tcset: unit -> tcset
       
    23   val TCSET: (tcset -> tactic) -> tactic
       
    24   val TCSET': (tcset -> 'a -> tactic) -> 'a -> tactic
    23   val AddTCs: thm list -> unit
    25   val AddTCs: thm list -> unit
    24   val DelTCs: thm list -> unit
    26   val DelTCs: thm list -> unit
    25   val TC_add_global: theory attribute
    27   val TC_add_global: theory attribute
    26   val TC_del_global: theory attribute
    28   val TC_del_global: theory attribute
    27   val TC_add_local: Proof.context attribute
    29   val TC_add_local: Proof.context attribute
   144 val tcset_of = tcset_of_sg o sign_of;
   146 val tcset_of = tcset_of_sg o sign_of;
   145 
   147 
   146 val tcset = tcset_of o Context.the_context;
   148 val tcset = tcset_of o Context.the_context;
   147 val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
   149 val tcset_ref = tcset_ref_of_sg o sign_of o Context.the_context;
   148 
   150 
       
   151 fun TCSET tacf st = tacf (tcset_of_sg (Thm.sign_of_thm st)) st;
       
   152 fun TCSET' tacf i st = tacf (tcset_of_sg (Thm.sign_of_thm st)) i st;
       
   153 
   149 
   154 
   150 (* change global tcset *)
   155 (* change global tcset *)
   151 
   156 
   152 fun change_tcset f x = tcset_ref () := (f (tcset (), x));
   157 fun change_tcset f x = tcset_ref () := (f (tcset (), x));
   153 
   158