Mercurial Mercurial > hg > nominal2 / 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.
merged
authorChristian Urban <urbanc@in.tum.de>
Wed, 13 Jan 2010 13:40:47 +0100
changeset 861 e3d17c4b3eca
parent 860 e18c691335db (diff)
parent 859 adadd0696472 (current diff)
child 863 6a27fc81c42f
merged
--- a/Quot/quotient_tacs.ML	Wed Jan 13 13:12:04 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 13 13:40:47 2010 +0100
@@ -29,10 +29,6 @@
 (* composition of two theorems, used in maps *)
 fun OF1 thm1 thm2 = thm2 RS thm1
 
-(* FIXME --- now in Isabelle *)
-fun SOLVED' tac i st =
-  tac i st |> Seq.filter (fn st' => nprems_of st' < nprems_of st)
-
 (* prints a warning, if the subgoal is not solved *)
 fun WARN (tac, msg) i st =
  case Seq.pull ((SOLVED' tac) i st) of
nominal2