author | wenzelm |
Thu, 11 Mar 2010 23:07:12 +0100 | |
changeset 35716 | 9dd4747d9591 |
parent 35715 | 9dc39bad4f4d |
child 35717 | 1856c0172cf2 |
--- a/src/Pure/assumption.ML Thu Mar 11 23:07:02 2010 +0100 +++ b/src/Pure/assumption.ML Thu Mar 11 23:07:12 2010 +0100 @@ -6,7 +6,7 @@ signature ASSUMPTION = sig - type export + type export = bool -> cterm list -> (thm -> thm) * (term -> term) val assume_export: export val presume_export: export val assume: cterm -> thm