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.
Removed "induct set" attribute from total induction rules
authorkrauss
Wed, 20 Sep 2006 12:05:31 +0200
changeset 20638 241792a4634e
parent 20637 d883e0fc1c51
child 20639 3aa960295c54
Removed "induct set" attribute from total induction rules
src/HOL/Tools/function_package/fundef_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 20 10:13:36 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 20 12:05:31 2006 +0200
@@ -135,7 +135,7 @@
         lthy
           |> add_simps "simps" [] mutual_info fixes tsimps stmts
           |> with_local_path defname
-                (LocalTheory.note (("induct", [Attrib.internal (InductAttrib.induct_set "")]), tinduct) #> snd)
+                (LocalTheory.note (("induct", []), tinduct) #> snd)
     end
isabelle