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.
adjusted qualified thm reference
authorhaftmann
Fri, 16 Mar 2007 21:32:19 +0100
changeset 22461 052cfe1c86dc
parent 22460 b4f96f343d6c
child 22462 2a93fb199302
adjusted qualified thm reference
src/HOL/Tools/function_package/fundef_core.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/function_package/fundef_core.ML	Fri Mar 16 21:32:18 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Fri Mar 16 21:32:19 2007 +0100
@@ -572,7 +572,7 @@
 (** Induction rule **)
 
 
-val acc_subset_induct = thm "FixedPoint.predicate1I" RS
+val acc_subset_induct = thm "Fun.predicate1I" RS
   thm "Accessible_Part.acc_subset_induct"
 
 fun mk_partial_induct_rule thy globals R complete_thm clauses =
isabelle