Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Wed, 08 Apr 2015 11:52:53 +0200
changeset 59953 3d207f8f40dd
parent 59952 550b74e9b08c
child 59955 0145010f3f83
child 59968 d69dc7a133e7
tuned signature;
src/HOL/Fun_Def.thy file | annotate | diff | comparison | revisions
src/HOL/Nominal/nominal_primrec.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/element.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/method.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/proof.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/rule_cases.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Fun_Def.thy	Wed Apr 08 11:52:35 2015 +0200
+++ b/src/HOL/Fun_Def.thy	Wed Apr 08 11:52:53 2015 +0200
@@ -103,7 +103,7 @@
 ML_file "Tools/Function/induction_schema.ML"
 
 method_setup induction_schema = {*
-  Scan.succeed (NO_CASES oo Induction_Schema.induction_schema_tac)
+  Scan.succeed (EMPTY_CASES oo Induction_Schema.induction_schema_tac)
 *} "prove an induction principle"
 
 
--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Apr 08 11:52:35 2015 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Apr 08 11:52:53 2015 +0200
@@ -374,7 +374,7 @@
         end)
       [goals] |>
     Proof.apply (Method.Basic (fn ctxt => fn _ =>
-      NO_CASES
+      EMPTY_CASES
        (rewrite_goals_tac ctxt defs_thms THEN
         compose_tac ctxt (false, rule, length rule_prems) 1))) |>
     Seq.hd
--- a/src/Pure/Isar/element.ML	Wed Apr 08 11:52:35 2015 +0200
+++ b/src/Pure/Isar/element.ML	Wed Apr 08 11:52:53 2015 +0200
@@ -276,7 +276,7 @@
 local
 
 val refine_witness =
-  Proof.refine (Method.Basic (fn ctxt => NO_CASES o
+  Proof.refine (Method.Basic (fn ctxt => EMPTY_CASES o
     K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (resolve_tac ctxt [Drule.protectI]))))))));
 
 fun gen_witness_proof proof after_qed wit_propss eq_props =
--- a/src/Pure/Isar/method.ML	Wed Apr 08 11:52:35 2015 +0200
+++ b/src/Pure/Isar/method.ML	Wed Apr 08 11:52:53 2015 +0200
@@ -90,8 +90,11 @@
 
 type method = thm list -> cases_tactic;
 
-fun METHOD_CASES tac : method = fn facts => Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts);
-fun METHOD tac : method = fn facts => NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts);
+fun METHOD_CASES tac : method =
+  fn facts => Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts);
+
+fun METHOD tac : method =
+  fn facts => EMPTY_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts);
 
 val fail = METHOD (K no_tac);
 val succeed = METHOD (K all_tac);
@@ -144,7 +147,7 @@
 fun atomize false ctxt =
       SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt)
   | atomize true ctxt =
-      NO_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
+      EMPTY_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
 
 
 (* this -- resolve facts directly *)
@@ -654,7 +657,7 @@
       "rotate assumptions of goal" #>
   setup @{binding tactic} (parse_tactic >> (K o METHOD))
     "ML tactic as proof method" #>
-  setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => NO_CASES o tac))
+  setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => EMPTY_CASES o tac))
     "ML tactic as raw proof method");
 
 
--- a/src/Pure/Isar/proof.ML	Wed Apr 08 11:52:35 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Apr 08 11:52:53 2015 +0200
@@ -884,7 +884,7 @@
   in map (Logic.mk_term o Var) vars end;
 
 fun refine_terms n =
-  refine (Method.Basic (fn ctxt => NO_CASES o
+  refine (Method.Basic (fn ctxt => EMPTY_CASES o
     K (HEADGOAL (PRECISE_CONJUNCTS n
       (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))))
   #> Seq.hd;
--- 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