Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -300 -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
Fri, 01 Aug 2014 23:33:43 +0200 blanchet tweaked 'clone' formula detection file | diff | annotate
Fri, 01 Aug 2014 23:29:50 +0200 blanchet fine-tuned Isar reconstruction, esp. boolean simplifications file | diff | annotate
Fri, 01 Aug 2014 23:29:49 +0200 blanchet centralized boolean simplification so that e.g. LEO-II benefits from it file | diff | annotate
Fri, 01 Aug 2014 20:44:29 +0200 blanchet better handling of variable names file | diff | annotate
Fri, 01 Aug 2014 20:08:50 +0200 blanchet nicer generated variable names file | diff | annotate
Fri, 01 Aug 2014 19:44:18 +0200 blanchet tuning file | diff | annotate
Fri, 01 Aug 2014 19:36:23 +0200 blanchet tuning file | diff | annotate
Fri, 01 Aug 2014 19:32:10 +0200 blanchet more precise handling of LEO-II skolemization file | diff | annotate
Fri, 01 Aug 2014 16:07:34 +0200 blanchet beware of 'skolem' rules that do not skolemize (e.g. LEO-II) file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet added appropriate method for skolemization of Z3 steps to the mix file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet tuning file | diff | annotate
Fri, 01 Aug 2014 14:43:57 +0200 blanchet eliminated Sledgehammer's "min" subcommand (and lots of complications in the code) file | diff | annotate
Wed, 30 Jul 2014 14:03:13 +0200 fleury Skolemization for tmp_ite_elim rule in the SMT solver veriT. file | diff | annotate
Wed, 30 Jul 2014 14:03:13 +0200 fleury Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma. file | diff | annotate
Wed, 30 Jul 2014 14:03:13 +0200 fleury Whitespace and indentation correction. file | diff | annotate
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch hilbert_choice_support file | diff | annotate
Wed, 30 Jul 2014 14:03:12 +0200 fleury veriT changes for lifted terms, and ite_elim rules. file | diff | annotate
Wed, 30 Jul 2014 14:03:12 +0200 fleury Subproofs for the SMT solver veriT. file | diff | annotate
Wed, 30 Jul 2014 14:03:12 +0200 fleury Basic support for the SMT prover veriT. file | diff | annotate
Wed, 30 Jul 2014 14:03:11 +0200 fleury Skolemization support for leo-II and Zipperposition. file | diff | annotate
Wed, 30 Jul 2014 00:50:41 +0200 blanchet also try 'metis' with 'full_types' file | diff | annotate
Thu, 24 Jul 2014 18:46:38 +0200 blanchet refined filter for ATP steps to avoid 'have True' steps in E proofs file | diff | annotate
Thu, 24 Jul 2014 18:46:38 +0200 blanchet 'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb) file | diff | annotate
Tue, 24 Jun 2014 08:19:22 +0200 blanchet supports gradual skolemization (cf. Z3) by threading context through correctly file | diff | annotate
Tue, 24 Jun 2014 08:19:22 +0200 blanchet given two one-liners, only show the best of the two file | diff | annotate
Tue, 24 Jun 2014 08:19:22 +0200 blanchet don't generate Isar proof skeleton for what amounts to a one-line proof file | diff | annotate
Thu, 12 Jun 2014 17:10:12 +0200 blanchet renamed Sledgehammer options file | diff | annotate
Mon, 02 Jun 2014 15:10:18 +0200 fleury basic setup for zipperposition prover file | diff | annotate
Thu, 22 May 2014 05:23:50 +0200 blanchet properly reconstruct helpers in Z3 proofs file | diff | annotate
Thu, 22 May 2014 03:29:36 +0200 blanchet tuning file | diff | annotate
Fri, 16 May 2014 19:14:00 +0200 blanchet correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs file | diff | annotate
Fri, 16 May 2014 19:13:50 +0200 blanchet use 'simp add:' syntax in Sledgehammer rather than 'using' file | diff | annotate
Sun, 04 May 2014 19:01:36 +0200 blanchet added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0') file | diff | annotate
Fri, 14 Mar 2014 11:44:11 +0100 blanchet consolidate consecutive steps that prove the same formula file | diff | annotate
Fri, 14 Mar 2014 11:15:46 +0100 blanchet undo rewrite rules (e.g. for 'fun_app') in Isar file | diff | annotate
Fri, 14 Mar 2014 11:05:45 +0100 blanchet debugging stuff file | diff | annotate
Fri, 14 Mar 2014 11:05:44 +0100 blanchet more simplification of trivial steps file | diff | annotate
Fri, 14 Mar 2014 11:05:37 +0100 blanchet tuning file | diff | annotate
Thu, 13 Mar 2014 13:18:14 +0100 blanchet tuning file | diff | annotate
Thu, 13 Mar 2014 13:18:14 +0100 blanchet simplified preplaying information file | diff | annotate
Thu, 13 Mar 2014 13:18:13 +0100 blanchet integrate SMT2 with Sledgehammer file | diff | annotate
Thu, 06 Mar 2014 10:12:47 +0100 wenzelm tuned signature; file | diff | annotate
Thu, 13 Feb 2014 13:16:17 +0100 blanchet avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures file | diff | annotate
Tue, 04 Feb 2014 23:11:18 +0100 blanchet more generous Isar proof compression -- try to remove failing steps file | diff | annotate
Tue, 04 Feb 2014 23:11:18 +0100 blanchet do a second phase of proof compression after minimization file | diff | annotate
Tue, 04 Feb 2014 23:11:18 +0100 blanchet tuned code file | diff | annotate
Tue, 04 Feb 2014 23:11:18 +0100 blanchet split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed) file | diff | annotate
Mon, 03 Feb 2014 23:59:36 +0100 blanchet rationalized lists of methods file | diff | annotate
Mon, 03 Feb 2014 23:49:01 +0100 blanchet extended method list file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet generate comments in Isar proofs file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet tuned behavior of 'smt' option file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet proper fresh name generation file | diff | annotate
Mon, 03 Feb 2014 17:13:31 +0100 blanchet added 'smt' option to control generation of 'by smt' proofs file | diff | annotate
Mon, 03 Feb 2014 16:53:58 +0100 blanchet renamed ML file file | diff | annotate
Mon, 03 Feb 2014 15:33:18 +0100 blanchet tuning file | diff | annotate
Mon, 03 Feb 2014 15:19:07 +0100 blanchet merged 'reconstructors' and 'proof methods' file | diff | annotate
Mon, 03 Feb 2014 13:37:23 +0100 blanchet tuning file | diff | annotate
Mon, 03 Feb 2014 11:58:38 +0100 blanchet tuned data structure file | diff | annotate
less more (0) -300 -100 -60 tip
isabelle