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.
prove_witness: context;
authorwenzelm
Sat, 08 Jul 2006 12:54:46 +0200
changeset 20058 7d035e26e5f9
parent 20057 058e913bac71
child 20059 25935807eb08
prove_witness: context;
src/Pure/Isar/element.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/element.ML	Sat Jul 08 12:54:45 2006 +0200
+++ b/src/Pure/Isar/element.ML	Sat Jul 08 12:54:46 2006 +0200
@@ -38,7 +38,7 @@
   val witness_prop: witness -> term
   val witness_hyps: witness -> term list
   val assume_witness: theory -> term -> witness
-  val prove_witness: theory -> term -> tactic -> witness
+  val prove_witness: Proof.context -> term -> tactic -> witness
   val conclude_witness: witness -> thm
   val mark_witness: term -> term
   val make_witness: term -> thm -> witness
@@ -274,8 +274,8 @@
 fun assume_witness thy t =
   Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t)));
 
-fun prove_witness thy t tac =
-  Witness (t, Goal.prove thy [] [] (Logic.protect t) (fn _ =>
+fun prove_witness ctxt t tac =
+  Witness (t, Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
     Tactic.rtac Drule.protectI 1 THEN tac));
 
 fun conclude_witness (Witness (_, th)) = Goal.norm_hhf (Goal.conclude th);
isabelle