Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/reflection.ML
changeset 31810 a6b800855cdd
parent 31794 71af1fd6a5e4
child 31986 a68f88d264f7 
--- a/src/HOL/Library/reflection.ML	Mon Jun 15 12:14:40 2009 +0200
+++ b/src/HOL/Library/reflection.ML	Mon Jun 08 18:37:35 2009 +0200
@@ -10,6 +10,7 @@
   val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
   val gen_reflection_tac: Proof.context -> (cterm -> thm)
     -> thm list -> thm list -> term option -> int -> tactic
+  val genreif : Proof.context -> thm list -> term -> thm
 end;
 
 structure Reflection : REFLECTION =
isabelle