Removed "induct set" attribute from total induction rules
authorkrauss
Wed Sep 20 12:05:31 2006 +0200 (2006-09-20)
changeset 20638241792a4634e
parent 20637 d883e0fc1c51
child 20639 3aa960295c54
Removed "induct set" attribute from total induction rules
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 20 10:13:36 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 20 12:05:31 2006 +0200
     1.3 @@ -135,7 +135,7 @@
     1.4          lthy
     1.5            |> add_simps "simps" [] mutual_info fixes tsimps stmts
     1.6            |> with_local_path defname
     1.7 -                (LocalTheory.note (("induct", [Attrib.internal (InductAttrib.induct_set "")]), tinduct) #> snd)
     1.8 +                (LocalTheory.note (("induct", []), tinduct) #> snd)
     1.9      end
    1.10  
    1.11