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.
more explicit name
authorblanchet
Tue, 05 Oct 2010 10:30:50 +0200
changeset 39949 186a3b447e0b
parent 39948 317010af8972
child 39950 f3c4849868b8
more explicit name
src/HOL/Tools/Meson/meson_clausify.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 05 10:28:11 2010 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 05 10:30:50 2010 +0200
@@ -213,7 +213,7 @@
     fun tacf [prem] =
       rewrite_goals_tac skolem_def_raw
       THEN rtac ((prem |> rewrite_rule skolem_def_raw)
-                 RS Global_Theory.get_thm thy "someI_ex") 1
+                 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
   in
     Goal.prove_internal [ex_tm] conc tacf
     |> forall_intr_list frees
isabelle