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.
Goal.norm_hhf_rule, Goal.init;
authorwenzelm
Fri, 21 Oct 2005 18:14:41 +0200
changeset 17961 6ebd59acf58a
parent 17960 5662fa033a92
child 17962 d4d2c854600b
Goal.norm_hhf_rule, Goal.init;
src/Provers/induct_method.ML file | annotate | diff | comparison | revisions 
--- a/src/Provers/induct_method.ML	Fri Oct 21 18:14:40 2005 +0200
+++ b/src/Provers/induct_method.ML	Fri Oct 21 18:14:41 2005 +0200
@@ -157,7 +157,7 @@
   Tactic.rewrite_goal_tac Data.rulify2 THEN'
   Tactic.norm_hhf_tac;
 
-val localize = Tactic.norm_hhf_rule o Tactic.simplify false Data.localize;
+val localize = Goal.norm_hhf_rule o Tactic.simplify false Data.localize;
 
 
 (* imp_intr --- limited to atomic prems *)
@@ -168,7 +168,7 @@
     val cprems = Drule.cprems_of th;
     val As = Library.take (length cprems - 1, cprems);
     val C = Thm.cterm_of (Thm.sign_of_thm th) (Var (("C", #maxidx (Thm.rep_thm th) + 1), propT));
-    val dummy_st = Drule.mk_triv_goal (Drule.list_implies (As, C));
+    val dummy_st = Goal.init (Drule.list_implies (As, C));
   in th COMP Thm.lift_rule (dummy_st, 1) Data.local_impI end;
isabelle