src/Pure/Isar/method.ML
changeset 11962 4c6585866fb2
parent 11905 77c63f8e9d9a
child 11971 2ee7c72cc464
equal deleted inserted replaced
11961:e5911a25d094 11962:4c6585866fb2
   678   ("succeed", no_args succeed, "succeed"),
   678   ("succeed", no_args succeed, "succeed"),
   679   ("-", no_args insert_facts, "do nothing (insert current facts only)"),
   679   ("-", no_args insert_facts, "do nothing (insert current facts only)"),
   680   ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
   680   ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"),
   681   ("unfold", thms_args unfold, "unfold definitions"),
   681   ("unfold", thms_args unfold, "unfold definitions"),
   682   ("fold", thms_args fold, "fold definitions"),
   682   ("fold", thms_args fold, "fold definitions"),
       
   683   ("atomize", no_args (SIMPLE_METHOD' HEADGOAL ObjectLogic.atomize_tac),
       
   684     "present local premises as object-level statements"),
   683   ("rule", thms_ctxt_args some_rule, "apply some rule"),
   685   ("rule", thms_ctxt_args some_rule, "apply some rule"),
   684   ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
   686   ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
   685   ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),
   687   ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),
   686   ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),
   688   ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"),
   687   ("this", no_args this, "apply current facts as rules"),
   689   ("this", no_args this, "apply current facts as rules"),