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.
keep rules with no premises in Isar proofs from veriT
authorblanchet
Tue, 30 Sep 2014 11:06:26 +0200
changeset 58489 558459615a73
parent 58488 289d1c39968c
child 58490 f6d99c69dae9
keep rules with no premises in Isar proofs from veriT
src/HOL/Tools/SMT/verit_isar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/SMT/verit_isar.ML	Tue Sep 30 10:25:04 2014 +0200
+++ b/src/HOL/Tools/SMT/verit_isar.ML	Tue Sep 30 11:06:26 2014 +0200
@@ -50,7 +50,7 @@
                   name0 :: normalizing_prems ctxt concl0)]
               end)
           end
-        else if rule = veriT_tmp_ite_elim_rule then
+        else if rule = veriT_tmp_ite_elim_rule orelse null prems then
           [standard_step Lemma]
         else
           [standard_step Plain]
isabelle