Fri, 22 Oct 2010 15:49:18 -0700 huffman rename lemma surjective_pairing_Sprod2 to spair_sfst_ssnd
Fri, 22 Oct 2010 15:47:43 -0700 huffman add lemma strict3
Fri, 22 Oct 2010 11:24:52 -0700 huffman do proofs using Rep_Sprod_simps, Rep_Ssum_simps; remove unused lemmas
Fri, 22 Oct 2010 07:45:32 -0700 huffman make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun
Fri, 22 Oct 2010 07:44:34 -0700 huffman direct instantiation unit :: discrete_cpo
Fri, 22 Oct 2010 06:58:45 -0700 huffman remove finite_po class
Fri, 22 Oct 2010 06:08:51 -0700 huffman simplify proofs about flift; remove unneeded lemmas
Fri, 22 Oct 2010 05:54:54 -0700 huffman simplify proof
Thu, 21 Oct 2010 15:21:39 -0700 huffman minimize imports
Thu, 21 Oct 2010 15:19:07 -0700 huffman add type annotation to avoid warning
Thu, 21 Oct 2010 12:51:36 -0700 huffman simplify some proofs, convert to Isar style
Thu, 21 Oct 2010 12:03:49 -0700 huffman rename lemma spair_lemma to spair_Sprod
Thu, 21 Oct 2010 06:03:18 -0700 huffman pcpodef (open) 'a lift
Thu, 21 Oct 2010 05:44:38 -0700 huffman remove intro! attribute from {sinl,sinr}_defined
Thu, 21 Oct 2010 05:35:32 -0700 huffman simplify proofs of ssumE, sprodE
Sun, 24 Oct 2010 21:25:13 +0200 wenzelm merged
Sun, 24 Oct 2010 20:37:30 +0200 nipkow renamed nat_number
Sun, 24 Oct 2010 20:19:00 +0200 nipkow nat_number -> eval_nat_numeral
Fri, 22 Oct 2010 23:45:20 +0200 krauss some cleanup in Function_Lib
Fri, 22 Oct 2010 17:15:46 +0200 blanchet merged
Fri, 22 Oct 2010 16:45:55 +0200 blanchet compile
Fri, 22 Oct 2010 16:37:11 +0200 blanchet added SMT solver to Sledgehammer docs
Fri, 22 Oct 2010 16:11:43 +0200 blanchet more robust handling of "remote_" vs. non-"remote_" provers
Fri, 22 Oct 2010 15:02:27 +0200 blanchet generalized the relevance filter so that it takes the list of "irrelevant constants" as argument (since the ATP and SMT preprocessing are different)
Fri, 22 Oct 2010 14:47:43 +0200 blanchet replaced references with proper record that's threaded through
Fri, 22 Oct 2010 14:10:32 +0200 blanchet fixed signature of "is_smt_solver_installed";
Fri, 22 Oct 2010 13:57:54 +0200 blanchet renamed modules
Fri, 22 Oct 2010 13:54:51 +0200 blanchet renamed files
Fri, 22 Oct 2010 13:49:44 +0200 blanchet took out "smt"/"remote_smt" from default ATPs until they are properly implemented
Fri, 22 Oct 2010 13:48:21 +0200 blanchet remove more needless code ("run_smt_solvers");
Fri, 22 Oct 2010 12:15:31 +0200 blanchet got rid of duplicate functionality ("run_smt_solver_somehow");
Fri, 22 Oct 2010 11:58:33 +0200 blanchet bring ATPs and SMT solvers more in line with each other
Fri, 22 Oct 2010 11:11:34 +0200 blanchet make Sledgehammer minimizer fully work with SMT
Fri, 22 Oct 2010 09:50:18 +0200 blanchet generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
Thu, 21 Oct 2010 16:25:40 +0200 blanchet first step in adding support for an SMT backend to Sledgehammer
Thu, 21 Oct 2010 14:55:09 +0200 blanchet use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
Thu, 21 Oct 2010 14:54:39 +0200 blanchet cosmetics
Fri, 22 Oct 2010 13:59:34 +0200 krauss relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version
Fri, 22 Oct 2010 12:01:12 +0200 hoelzl Changed section title to please LaTeX.
Thu, 21 Oct 2010 20:26:35 +0200 bulwahn temporary removed Predicate_Compile_Quickcheck_Examples from tests
Thu, 21 Oct 2010 19:13:11 +0200 bulwahn adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
Thu, 21 Oct 2010 19:13:10 +0200 bulwahn using a signature in core_data and moving some more functions to core_data
Thu, 21 Oct 2010 19:13:09 +0200 bulwahn splitting large core file into core_data, mode_inference and predicate_compile_proof
Thu, 21 Oct 2010 19:13:09 +0200 bulwahn added generator_dseq compilation for a sound depth-limited compilation with small value generators
Thu, 21 Oct 2010 19:13:08 +0200 bulwahn for now safely but unpractically assume no predicate is terminating
Thu, 21 Oct 2010 19:13:07 +0200 bulwahn adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
Thu, 21 Oct 2010 19:13:06 +0200 bulwahn adding option smart_depth_limiting to predicate compiler
Wed, 20 Oct 2010 21:26:51 -0700 huffman merged
Wed, 20 Oct 2010 19:40:02 -0700 huffman introduce function strict :: 'a -> 'b -> 'b, which works like Haskell's seq; use strict instead of strictify in various definitions
Wed, 20 Oct 2010 17:25:22 -0700 huffman add lemma lub_eq_bottom_iff
Wed, 20 Oct 2010 16:19:25 -0700 huffman combine check_and_sort_domain with main function; rewrite much of the error-checking code
Wed, 20 Oct 2010 13:22:30 -0700 huffman constructor arguments with selectors must have pointed types
Wed, 20 Oct 2010 13:02:13 -0700 huffman simplify check_and_sort_domain; more meaningful variable names
Tue, 19 Oct 2010 16:21:24 -0700 huffman replace fixrec 'permissive' mode with per-equation 'unchecked' option
Tue, 19 Oct 2010 15:01:51 -0700 huffman rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML
Tue, 19 Oct 2010 14:28:14 -0700 huffman simplify some proofs; remove some unused lists of lemmas
Tue, 19 Oct 2010 11:07:42 -0700 huffman replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function
Tue, 19 Oct 2010 10:13:29 -0700 huffman eliminate constant 'coerce'; use 'prj oo emb' instead
Tue, 19 Oct 2010 07:05:04 -0700 huffman simplify fixrec pattern match function
Sun, 17 Oct 2010 09:53:47 -0700 huffman simplify some proofs
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip