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.
fixed function package bug in the handling of multiple guards
authorkrauss
Tue, 06 Mar 2007 15:49:25 +0100
changeset 22419 17441293ebc6
parent 22418 49e2d9744ae1
child 22420 4ccc8c1b08a3
fixed function package bug in the handling of multiple guards
src/HOL/Tools/function_package/fundef_core.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/function_package/fundef_core.ML	Tue Mar 06 15:28:22 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Tue Mar 06 15:49:25 2007 +0100
@@ -628,7 +628,7 @@
     val P_lhs = assume step
            |> fold forall_elim cqs
            |> implies_elim_swp lhs_D 
-           |> fold_rev implies_elim_swp ags
+           |> fold implies_elim_swp ags
            |> fold implies_elim_swp P_recs
           
     val res = cterm_of thy (Trueprop (P $ x))
isabelle