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.prove_plain;
authorwenzelm
Fri, 21 Oct 2005 18:14:53 +0200
changeset 17973 ef2c44da2f68
parent 17972 4969d6eb4c97
child 17974 5b54db4a44ee
Goal.prove_plain;
src/Pure/Isar/locale.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/locale.ML	Fri Oct 21 18:14:52 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Oct 21 18:14:53 2005 +0200
@@ -1907,7 +1907,7 @@
 
     val cert = Thm.cterm_of defs_thy;
 
-    val intro = Drule.standard (Tactic.prove defs_thy [] norm_ts statement (fn _ =>
+    val intro = Drule.standard (Goal.prove defs_thy [] norm_ts statement (fn _ =>
       Tactic.rewrite_goals_tac [pred_def] THEN
       Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
       Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1));
@@ -1917,7 +1917,7 @@
         Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
       |> Drule.conj_elim_precise (length ts);
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
-      Tactic.prove_plain defs_thy [] [] t (fn _ =>
+      Goal.prove_plain defs_thy [] [] t (fn _ =>
         Tactic.rewrite_goals_tac defs THEN
         Tactic.compose_tac (false, ax, 0) 1));
   in (defs_thy, (statement, intro, axioms)) end;
isabelle