| changeset 32734 | 06c13b2e562e |
| parent 32733 | 71618deaf777 |
| child 32740 | 9dd0a2f83429 |
--- a/src/HOL/HOL.thy Mon Sep 28 22:47:34 2009 +0200 +++ b/src/HOL/HOL.thy Mon Sep 28 23:13:37 2009 +0200 @@ -1469,7 +1469,7 @@ subsubsection {* Coherent logic *} ML {* -structure Coherent = CoherentFun +structure Coherent = Coherent ( val atomize_elimL = @{thm atomize_elimL} val atomize_exL = @{thm atomize_exL}