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.
InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;
authorwenzelm
Sat, 14 Jun 2008 23:20:09 +0200
changeset 27216 dc1455f96f56
parent 27215 b43785a81e01
child 27217 ddce31131fee
InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove;
src/HOL/Nominal/nominal_atoms.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Jun 14 23:20:07 2008 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Jun 14 23:20:09 2008 +0200
@@ -95,7 +95,7 @@
                   (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
 
               val proof2 = fn {prems, context} =>
-                InductTacs.case_tac (context |> Variable.declare_term y) ("y", NONE) 1 THEN
+                InductTacs.case_tac context "y" 1 THEN
                 asm_simp_tac (HOL_basic_ss addsimps simp1) 1 THEN
                 rtac @{thm exI} 1 THEN
                 rtac @{thm refl} 1
isabelle