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.
Theorems for converting between wf and wfP are now declared
authorberghofe
Wed, 07 Feb 2007 17:30:53 +0100
changeset 22264 6a65e9b2ae05
parent 22263 990a638e6f69
child 22265 3c5c6bdf61de
Theorems for converting between wf and wfP are now declared as hints.
src/HOL/Recdef.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Recdef.thy	Wed Feb 07 17:29:41 2007 +0100
+++ b/src/HOL/Recdef.thy	Wed Feb 07 17:30:53 2007 +0100
@@ -79,6 +79,8 @@
   wf_pred_nat
   wf_same_fst
   wf_empty
+  wf_implies_wfP
+  wfP_implies_wf
 
 (* The following should really go into Datatype or Finite_Set, but
 each one lacks the other theory as a parent . . . *)
isabelle