Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Thu, 14 Apr 2011 11:24:05 +0200 properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
changeset
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42347
properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code
Thu, 14 Apr 2011 11:24:05 +0200 remove experimental code added in 85bb6fbb8e6a
changeset
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42346
remove experimental code added in 85bb6fbb8e6a
Thu, 14 Apr 2011 11:24:05 +0200 added examples of definitional CNF facts
changeset
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42345
added examples of definitional CNF facts
Thu, 14 Apr 2011 11:24:05 +0200 "unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
changeset
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42344
"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
Thu, 14 Apr 2011 11:24:05 +0200 compile
changeset
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42343
compile
Thu, 14 Apr 2011 11:24:05 +0200 handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
changeset
blanchet [Thu, 14 Apr 2011 11:24:05 +0200] rev 42342
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle