src/HOL/HOL.thy
changeset 31299 0c5baf034d0e
parent 31173 bbe9e29b9672
child 31804 627d142fce19
     1.1 --- a/src/HOL/HOL.thy	Sat May 30 11:57:36 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat May 30 12:52:57 2009 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4    ("Tools/recfun_codegen.ML")
     1.5  begin
     1.6  
     1.7 -setup {* Intuitionistic.method_setup "iprover" *}
     1.8 +setup {* Intuitionistic.method_setup @{binding iprover} *}
     1.9  
    1.10  
    1.11  subsection {* Primitive logic *}