Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
Wed, 21 Oct 2020 17:46:51 +0200 desharna Tuned isar_proofs constructions file | diff | annotate
Wed, 21 Oct 2020 17:31:15 +0200 desharna Tuned isar_proof datatype file | diff | annotate
Thu, 08 Oct 2020 17:46:03 +0200 blanchet removed obsolete unmaintained experimental prover Pirate file | diff | annotate
Tue, 20 Aug 2019 11:01:05 +0200 wenzelm clarified signature; file | diff | annotate
Mon, 03 Jun 2019 15:40:08 +0200 wenzelm clarified signature; file | diff | annotate
Thu, 11 Jan 2018 13:48:17 +0100 wenzelm uniform use of Standard ML op-infix -- eliminated warnings; file | diff | annotate
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources file | diff | annotate
Tue, 06 Jun 2017 13:13:25 +0200 wenzelm discontinued obsolete print mode; file | diff | annotate
Mon, 30 Nov 2015 13:16:12 +0100 blanchet avoid 'hence' and 'thus' in generated proofs file | diff | annotate
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2}; file | diff | annotate
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; file | diff | annotate
Mon, 29 Sep 2014 10:39:39 +0200 blanchet make sure no '__' suffixes make it until Isar proof file | diff | annotate
Mon, 29 Sep 2014 10:39:39 +0200 blanchet rename skolem symbols in the negative case as well file | diff | annotate
Thu, 28 Aug 2014 19:02:37 +0200 blanchet use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example) file | diff | annotate
Thu, 28 Aug 2014 16:58:27 +0200 blanchet generate 'thesis' variable in Sledgehammer Isar proofs file | diff | annotate
Thu, 28 Aug 2014 16:58:26 +0200 blanchet three-line 'obtain' format for generated Isar proofs file | diff | annotate
Thu, 28 Aug 2014 00:40:37 +0200 blanchet reintroduced two-line-per-inference Isar proof format file | diff | annotate
Tue, 05 Aug 2014 11:07:53 +0200 blanchet tuned skolemization file | diff | annotate
Tue, 05 Aug 2014 10:59:40 +0200 blanchet rationalize Skolem names file | diff | annotate
Mon, 04 Aug 2014 12:28:42 +0200 blanchet rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures 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, 25 Jul 2014 11:26:11 +0200 blanchet more robustness in Isar proof construction file | diff | annotate
Thu, 24 Jul 2014 18:46:38 +0200 blanchet introduce fact chaining also under first step 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
Mon, 02 Jun 2014 15:10:18 +0200 fleury basic setup for zipperposition prover 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
Thu, 13 Mar 2014 13:18:13 +0100 blanchet integrate SMT2 with Sledgehammer file | diff | annotate
Mon, 03 Feb 2014 23:44:39 +0100 blanchet don't lose additional outcomes file | diff | annotate
Mon, 03 Feb 2014 19:32:02 +0100 blanchet generate comments in Isar proofs file | diff | annotate
Mon, 03 Feb 2014 16:53:58 +0100 blanchet renamed ML file file | diff | annotate
Mon, 03 Feb 2014 15:19:07 +0100 blanchet merged 'reconstructors' and 'proof methods' file | diff | annotate
Mon, 03 Feb 2014 14:35:19 +0100 blanchet added 'smt' as a proof method file | diff | annotate
Mon, 03 Feb 2014 13:37:23 +0100 blanchet tuning file | diff | annotate
Mon, 03 Feb 2014 13:35:50 +0100 blanchet refactor relabeling code file | diff | annotate
Mon, 03 Feb 2014 11:58:38 +0100 blanchet tuned data structure file | diff | annotate
Mon, 03 Feb 2014 11:37:48 +0100 blanchet tuned data structure file | diff | annotate
Mon, 03 Feb 2014 11:30:53 +0100 blanchet more flexible compression, choosing whichever proof method works file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet more data structure rationalization file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet rationalized threading of 'metis' arguments file | diff | annotate
Sun, 02 Feb 2014 20:53:51 +0100 blanchet simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods file | diff | annotate
Fri, 31 Jan 2014 19:16:41 +0100 blanchet generalized preplaying infrastructure to store various results for various methods file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet added a 'trace' option file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet moved code around file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet added 'algebra' to the mix file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet more informative trace file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet tuning file | diff | annotate
Fri, 31 Jan 2014 18:43:16 +0100 blanchet more concise Isar output file | diff | annotate
Fri, 31 Jan 2014 16:41:54 +0100 blanchet better tracing + syntactically correct 'metis' calls file | diff | annotate
Fri, 31 Jan 2014 16:26:43 +0100 blanchet tuned ML function names file | diff | annotate
Fri, 31 Jan 2014 16:10:39 +0100 blanchet tuning file | diff | annotate
Fri, 31 Jan 2014 16:07:20 +0100 blanchet moved ML code around file | diff | annotate
Fri, 31 Jan 2014 10:23:32 +0100 blanchet renamed many Sledgehammer ML files to clarify structure file | diff | annotate | base
less more (0) tip
isabelle