Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/atp_translate.ML
Sat, 29 Oct 2011 13:15:58 +0200 blanchet added sorted DFG output for coming version of SPASS file | diff | annotate
Sat, 29 Oct 2011 13:15:58 +0200 blanchet check "sound" flag before doing something unsound... file | diff | annotate
Wed, 19 Oct 2011 16:36:13 +0200 blanchet avoid generating too meta theorems -- this sometimes leads to type errors, e.g. when "pp" is applied to a "prop" instead of a "bool" file | diff | annotate
Tue, 18 Oct 2011 15:40:59 +0200 blanchet freeze conjecture schematics before applying lambda-translation, which sometimes calls "close_form" and ruins it for freezing file | diff | annotate
Tue, 18 Oct 2011 15:40:58 +0200 blanchet gracefully handle quantifiers of the form "All $ t" where "t" is not a lambda-abstraction in higher-order translations file | diff | annotate
Sat, 10 Sep 2011 00:44:25 +0200 blanchet fixed definition of type intersection (soundness bug) file | diff | annotate
Fri, 09 Sep 2011 14:30:57 +0200 blanchet made SML/NJ happy file | diff | annotate
Thu, 08 Sep 2011 09:25:55 +0200 blanchet fixed computation of "in_conj" for polymorphic encodings file | diff | annotate
Wed, 07 Sep 2011 21:31:21 +0200 blanchet also implemented ghost version of the tagged encodings file | diff | annotate
Wed, 07 Sep 2011 21:31:21 +0200 blanchet smarter explicit apply business file | diff | annotate
Wed, 07 Sep 2011 21:31:21 +0200 blanchet started work on ghost type arg encoding file | diff | annotate
Wed, 07 Sep 2011 21:31:21 +0200 blanchet stricted type encoding parsing file | diff | annotate
Wed, 07 Sep 2011 13:50:17 +0200 blanchet tweaking polymorphic TFF and THF output file | diff | annotate
Wed, 07 Sep 2011 13:50:17 +0200 blanchet parse new experimental '@' encodings file | diff | annotate
Wed, 07 Sep 2011 13:50:17 +0200 blanchet tuning file | diff | annotate
Wed, 07 Sep 2011 13:50:16 +0200 blanchet tuning file | diff | annotate
Wed, 07 Sep 2011 09:10:41 +0200 blanchet separate mangling, which can (and should) be done before the formulas are first-orderized, and type arg filtering, which must be done after once the min arities have been computed file | diff | annotate
Wed, 07 Sep 2011 09:10:41 +0200 blanchet perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s file | diff | annotate
Wed, 07 Sep 2011 09:10:41 +0200 blanchet tuning file | diff | annotate
Wed, 07 Sep 2011 09:10:41 +0200 blanchet make mangling sound w.r.t. type arguments file | diff | annotate
Wed, 07 Sep 2011 09:10:41 +0200 blanchet make "filter_type_args" more robust if the actual arity is higher than the declared one file | diff | annotate
Wed, 07 Sep 2011 09:10:41 +0200 blanchet rationalize uniform encodings file | diff | annotate
Tue, 06 Sep 2011 18:13:36 +0200 blanchet added dummy polymorphic THF system file | diff | annotate
Tue, 06 Sep 2011 11:31:01 +0200 blanchet cleanup "simple" type encodings file | diff | annotate
Tue, 06 Sep 2011 09:11:08 +0200 blanchet drop more type arguments soundly, when they can be deduced from the arg types file | diff | annotate
Thu, 01 Sep 2011 13:18:27 +0200 blanchet make "sound" sound and "unsound" more sound, based on evaluation file | diff | annotate
Wed, 31 Aug 2011 13:22:50 +0200 blanchet make SML/NJ happy file | diff | annotate
Wed, 31 Aug 2011 11:52:03 +0200 blanchet more tuning file | diff | annotate
Wed, 31 Aug 2011 11:23:16 +0200 blanchet more tuning file | diff | annotate
Wed, 31 Aug 2011 11:14:53 +0200 blanchet tuning file | diff | annotate
Wed, 31 Aug 2011 11:12:27 +0200 blanchet avoid relying on dubious TFF1 feature file | diff | annotate
Tue, 30 Aug 2011 16:07:46 +0200 blanchet generate properly typed TFF1 (PFF) problems in the presence of type class predicates file | diff | annotate
Tue, 30 Aug 2011 16:07:45 +0200 blanchet added type abstractions (for declaring polymorphic constants) to TFF syntax file | diff | annotate
Tue, 30 Aug 2011 16:07:45 +0200 blanchet implement more of the polymorphic simply typed format TFF(1) file | diff | annotate
Tue, 30 Aug 2011 16:07:45 +0200 blanchet extended simple types with polymorphism -- the implementation still needs some work though file | diff | annotate
Tue, 30 Aug 2011 16:07:34 +0200 blanchet first step towards polymorphic TFF + changed defaults for Vampire file | diff | annotate
Tue, 30 Aug 2011 14:29:39 +0200 nik removed explicit reliance on Hilbert_Choice.Eps file | diff | annotate
Tue, 30 Aug 2011 14:12:55 +0200 nik improved handling of induction rules in Sledgehammer file | diff | annotate
Tue, 30 Aug 2011 14:12:55 +0200 nik added generation of induction rules file | diff | annotate
Fri, 26 Aug 2011 21:52:11 +0200 blanchet change default for generation of tag idempotence and tag argument equations file | diff | annotate
Fri, 26 Aug 2011 10:12:17 +0200 blanchet comment file | diff | annotate
Fri, 26 Aug 2011 01:14:49 +0200 blanchet improve completeness of polymorphic encodings file | diff | annotate
Fri, 26 Aug 2011 00:19:25 +0200 blanchet mangle tag bound declarations properly file | diff | annotate
Fri, 26 Aug 2011 00:05:45 +0200 blanchet fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings file | diff | annotate
Thu, 25 Aug 2011 23:54:57 +0200 blanchet honor TFF Implicit file | diff | annotate
Thu, 25 Aug 2011 23:38:09 +0200 blanchet make polymorphic encodings more complete file | diff | annotate
Thu, 25 Aug 2011 22:06:25 +0200 blanchet make default unsound mode less unsound file | diff | annotate
Thu, 25 Aug 2011 22:05:18 +0200 blanchet make TFF output less explicit where possible file | diff | annotate
Thu, 25 Aug 2011 19:02:47 +0200 blanchet added config options to control two aspects of the translation, for evaluation purposes file | diff | annotate
Thu, 25 Aug 2011 13:55:52 +0100 nik added choice operator output for file | diff | annotate
Thu, 25 Aug 2011 14:25:07 +0200 blanchet rationalized option names -- mono becomes raw_mono and mangled becomes mono file | diff | annotate
Thu, 25 Aug 2011 14:25:07 +0200 blanchet handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper -- otherwise we can end up generating too tight type guards file | diff | annotate
Thu, 25 Aug 2011 14:25:06 +0200 blanchet fixed bang encoding detection of which types to encode file | diff | annotate
Wed, 24 Aug 2011 15:25:39 +0200 blanchet make sure that all facts are passed to ATP from minimizer file | diff | annotate
Wed, 24 Aug 2011 11:17:33 +0200 blanchet tuning file | diff | annotate
Tue, 23 Aug 2011 23:18:13 +0200 blanchet fixed "hBOOL" of existential variables, and generate more helpers file | diff | annotate
Tue, 23 Aug 2011 14:44:19 +0200 blanchet fixed TFF slicing file | diff | annotate
Tue, 23 Aug 2011 14:44:19 +0200 blanchet added formats to the slice and use TFF for remote Vampire file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet we must tag any type whose ground types intersect a nonmonotonic type file | diff | annotate
Mon, 22 Aug 2011 15:02:45 +0200 blanchet made reconstruction of type tag equalities "\?x = \?x" reliable file | diff | annotate
less more (0) -100 -60 tip
isabelle