src/Pure/Isar/attrib.ML
changeset 6874 747f656e04ec
parent 6846 f2380295d4dd
child 6933 0890fde41522
equal deleted inserted replaced
6873:b123f5522ea1 6874:747f656e04ec
   260 val pure_attributes =
   260 val pure_attributes =
   261  [("tag", (gen_tag, gen_tag), "tag theorem"),
   261  [("tag", (gen_tag, gen_tag), "tag theorem"),
   262   ("untag", (gen_untag, gen_untag), "untag theorem"),
   262   ("untag", (gen_untag, gen_untag), "untag theorem"),
   263   ("COMP", (global_COMP, local_COMP), "compose rules (no lifting)"),
   263   ("COMP", (global_COMP, local_COMP), "compose rules (no lifting)"),
   264   ("RS", (global_RS, local_RS), "resolve with rule"),
   264   ("RS", (global_RS, local_RS), "resolve with rule"),
   265   ("APP", (global_APP, local_APP), "resolve rule with"),
   265   ("OF", (global_APP, local_APP), "resolve with rule -- apply rule to rules"),
   266   ("where", (global_where, local_where), "named instantiation of theorem"),
   266   ("where", (global_where, local_where), "named instantiation of theorem"),
   267   ("with", (global_with, local_with), "positional instantiation of theorem"),
   267   ("of", (global_with, local_with), "positional instantiation of theorem -- apply rule to terms"),
   268   ("standard", (standard, standard), "put theorem into standard form"),
   268   ("standard", (standard, standard), "put theorem into standard form"),
   269   ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"),
   269   ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"),
   270   ("transfer", (global_transfer, local_transfer), "transfer theorem to this theory")];
   270   ("transfer", (global_transfer, local_transfer), "transfer theorem to this theory")];
   271 
   271 
   272 
   272