Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/rule_cases.ML
changeset 59953 3d207f8f40dd
parent 59660 49e498cedd02
child 59970 e9f73d87d904 
--- a/src/Pure/Isar/rule_cases.ML	Wed Apr 08 11:52:35 2015 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Wed Apr 08 11:52:53 2015 +0200
@@ -12,7 +12,7 @@
   type cases_state = cases * thm
   type cases_tactic = thm -> cases_state Seq.seq
   val CASES: cases -> tactic -> cases_tactic
-  val NO_CASES: tactic -> cases_tactic
+  val EMPTY_CASES: tactic -> cases_tactic
   val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic
   val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
 end
@@ -188,7 +188,7 @@
 type cases_tactic = thm -> cases_state Seq.seq;
 
 fun CASES cases tac st = Seq.map (pair cases) (tac st);
-fun NO_CASES tac = CASES [] tac;
+fun EMPTY_CASES tac = CASES [] tac;
 
 fun SUBGOAL_CASES tac i st =
   (case try Logic.nth_prem (i, Thm.prop_of st) of
isabelle