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.
Coercion_Examples defines required coercions itself (no Complex_Main needed)
authortraytel
Fri, 22 Feb 2013 13:38:10 +0100
changeset 51247 064683ba110c
parent 51246 755562fd2d9d
child 51248 029de23bb5e8
Coercion_Examples defines required coercions itself (no Complex_Main needed)
src/HOL/ex/Coercion_Examples.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/Coercion_Examples.thy	Fri Feb 22 13:36:31 2013 +0100
+++ b/src/HOL/ex/Coercion_Examples.thy	Fri Feb 22 13:38:10 2013 +0100
@@ -5,9 +5,11 @@
 *)
 
 theory Coercion_Examples
-imports Complex_Main
+imports Main
 begin
 
+declare[[coercion_enabled]]
+
 (* Error messages test *)
 
 consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"
isabelle