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.
merge
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 13 Jan 2010 15:17:52 +0100
changeset 863 6a27fc81c42f
parent 862 09ec51d50fc6 (current diff)
parent 861 e3d17c4b3eca (diff)
child 864 999870716cc8
merge
--- a/Quot/quotient_tacs.ML	Wed Jan 13 15:17:36 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 13 15:17:52 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