src/Pure/Isar/calculation.ML
changeset 8150 7021549ef32d
parent 7600 73f91da46230
child 8300 4c3f83414de3
equal deleted inserted replaced
8149:941afb897532 8150:7021549ef32d
    81 
    81 
    82 (* trans add/del *)
    82 (* trans add/del *)
    83 
    83 
    84 local
    84 local
    85 
    85 
    86 fun map_rules_global f thy = GlobalCalculation.put (f (GlobalCalculation.get thy)) thy;
       
    87 fun map_rules_local f ctxt = LocalCalculation.put (f (LocalCalculation.get ctxt)) ctxt;
       
    88 
       
    89 fun add_trans thm rules = Library.gen_ins Thm.eq_thm (thm, rules);
    86 fun add_trans thm rules = Library.gen_ins Thm.eq_thm (thm, rules);
    90 fun del_trans thm rules = Library.gen_rem Thm.eq_thm (rules, thm);
    87 fun del_trans thm rules = Library.gen_rem Thm.eq_thm (rules, thm);
    91 
    88 
    92 fun mk_att f g (x, thm) = (f (g thm) x, thm);
    89 fun mk_att f g (x, thm) = (f (g thm) x, thm);
    93 
    90 
    94 in
    91 in
    95 
    92 
    96 val trans_add_global = mk_att map_rules_global add_trans;
    93 val trans_add_global = mk_att GlobalCalculation.map add_trans;
    97 val trans_del_global = mk_att map_rules_global del_trans;
    94 val trans_del_global = mk_att GlobalCalculation.map del_trans;
    98 val trans_add_local = mk_att map_rules_local (Library.apfst o add_trans);
    95 val trans_add_local = mk_att LocalCalculation.map (Library.apfst o add_trans);
    99 val trans_del_local = mk_att map_rules_local (Library.apfst o del_trans);
    96 val trans_del_local = mk_att LocalCalculation.map (Library.apfst o del_trans);
   100 
    97 
   101 end;
    98 end;
   102 
    99 
   103 
   100 
   104 (* concrete syntax *)
   101 (* concrete syntax *)