Mercurial Mercurial > repos > isabelle / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -10000 -1024 +1024 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
Mon, 06 Dec 2010 16:18:56 +0100 wenzelm merged changeset | files
Mon, 06 Dec 2010 13:46:45 +0100 blanchet fix monotonicity type of None changeset | files
Mon, 06 Dec 2010 13:36:28 +0100 blanchet compile changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet introduced hack to exploit the symmetry of equality in monotonicity calculus changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet cleanup example changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet add more flexibility to the monotonicity calculus: instead of hardcoding F-arrows, also allow G-arrows, simulating applications of the Sub rule changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet fixed bug in monotonicity solution display, whereby the polarity of literals was ignored changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet improve precision of forall in constancy part of the monotonicity calculus changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet added some missing well-annotatedness constraints to monotonicity calculus changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet more work on the monotonicity evaluation driver changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet improve precision of finite functions in monotonicity calculus changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet added ML code for testing entire theories for monotonicity changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout -- this becomes necessary with the new, more powerful monotonicity calculus changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet added examples to exercise new monotonicity code changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet fixed quantifier handling of new monotonicity calculus changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet tune parentheses and indentation changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet proper handling of frames for connectives in monotonicity calculus changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet tune indentation changeset | files
Mon, 06 Dec 2010 13:33:09 +0100 blanchet removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications changeset | files
Mon, 06 Dec 2010 13:33:05 +0100 blanchet implemented All rules from new monotonicity calculus changeset | files
Mon, 06 Dec 2010 13:30:57 +0100 blanchet fixed bug in clause handling in monotonicity code, whereby the unsound rule False | x <--> False was used to simplify constraints changeset | files
Mon, 06 Dec 2010 13:30:38 +0100 blanchet started implementing the new monotonicity rules for application changeset | files
Mon, 06 Dec 2010 13:30:36 +0100 blanchet implemented connectives in new monotonicity calculus changeset | files
Mon, 06 Dec 2010 13:29:23 +0100 blanchet added "Neq" operator to monotonicity inference module changeset | files
Mon, 06 Dec 2010 13:26:27 +0100 blanchet started implementing connectives in new monotonicity calculus changeset | files
Mon, 06 Dec 2010 13:26:23 +0100 blanchet more work on frames in the new monotonicity calculus changeset | files
Mon, 06 Dec 2010 13:18:25 +0100 blanchet support 3 monotonicity calculi in one and fix soundness bug changeset | files
Mon, 06 Dec 2010 13:18:25 +0100 blanchet tuning changeset | files
Mon, 06 Dec 2010 13:18:25 +0100 blanchet proper handling of assignment disjunctions vs. conjunctions changeset | files
Mon, 06 Dec 2010 13:18:25 +0100 blanchet adapt monotonicity code to four annotation types changeset | files
Mon, 06 Dec 2010 13:18:25 +0100 blanchet more monotonicity tuning changeset | files
Mon, 06 Dec 2010 13:18:25 +0100 blanchet tuning changeset | files
Mon, 06 Dec 2010 13:18:25 +0100 blanchet added frame component to Gamma in monotonicity calculus changeset | files
Mon, 06 Dec 2010 13:18:25 +0100 blanchet use boolean pair to encode annotation, which may now take four values changeset | files
Mon, 06 Dec 2010 13:18:25 +0100 blanchet started generalizing monotonicity code to accommodate new calculus changeset | files
Mon, 06 Dec 2010 13:17:26 +0100 blanchet merged changeset | files
Mon, 06 Dec 2010 11:41:24 +0100 blanchet handle "max_relevant" uniformly changeset | files
Mon, 06 Dec 2010 11:26:17 +0100 blanchet honor the default max relevant facts setting from the SMT solvers in Sledgehammer changeset | files
Mon, 06 Dec 2010 11:25:21 +0100 blanchet have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts? changeset | files
Mon, 06 Dec 2010 10:32:39 +0100 blanchet return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction changeset | files
Mon, 06 Dec 2010 10:31:29 +0100 blanchet trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases changeset | files
Mon, 06 Dec 2010 10:23:31 +0100 blanchet reraise interrupt exceptions changeset | files
Mon, 06 Dec 2010 09:54:58 +0100 blanchet [mq]: sledge_binary_minimizer changeset | files
Mon, 06 Dec 2010 10:52:48 +0100 bulwahn correcting usage documentation in mirabelle tool changeset | files
Mon, 06 Dec 2010 10:52:46 +0100 bulwahn adding mutabelle as a component and an isabelle tool to be used in regression testing changeset | files
Mon, 06 Dec 2010 10:52:45 +0100 bulwahn commenting out sledgehammer_mtd in Mutabelle changeset | files
Mon, 06 Dec 2010 10:52:45 +0100 bulwahn removing declaration in quickcheck to really enable exhaustive testing changeset | files
Mon, 06 Dec 2010 10:52:44 +0100 bulwahn adding timeout to try invocation in mutabelle changeset | files
Mon, 06 Dec 2010 10:52:43 +0100 bulwahn adding filtering, sytactic welltyping, and sledgehammer method in mutabelle changeset | files
Mon, 06 Dec 2010 09:34:57 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting` changeset | files
Mon, 06 Dec 2010 09:25:05 +0100 haftmann moved bootstrap of type_lifting to Fun changeset | files
Mon, 06 Dec 2010 09:19:10 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting` changeset | files
Mon, 06 Dec 2010 14:45:29 +0100 wenzelm avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle; changeset | files
Sun, 05 Dec 2010 15:23:33 +0100 wenzelm IsabelleText font: include Cyrillic, Hebrew, Arabic from DejaVu Sans 2.32; changeset | files
Sun, 05 Dec 2010 14:02:16 +0100 wenzelm command 'notepad' replaces former 'example_proof'; changeset | files
Sun, 05 Dec 2010 13:42:58 +0100 wenzelm prefer 'notepad' over 'example_proof'; changeset | files
Sun, 05 Dec 2010 08:34:02 +0100 haftmann merged changeset | files
Sat, 04 Dec 2010 21:53:00 +0100 haftmann more intimate definition of fold_list / fold_once in terms of fold changeset | files
Sat, 04 Dec 2010 21:26:33 +0100 haftmann canonical fold signature changeset | files
Sat, 04 Dec 2010 21:26:55 +0100 wenzelm formal notepad without any result; changeset | files
Sat, 04 Dec 2010 18:41:12 +0100 wenzelm added Syntax.default_root; changeset | files
Sat, 04 Dec 2010 15:14:28 +0100 wenzelm eliminated obsolete Token.Malformed -- subsumed by Token.Error; changeset | files
Sat, 04 Dec 2010 14:59:25 +0100 wenzelm tuned @{datatype} using Syntax.pretty_priority (NB: postfix type application yields Syntax.max_pri, so arguments in prefix application require higher priority); changeset | files
Sat, 04 Dec 2010 14:57:04 +0100 wenzelm added Syntax.pretty_priority; changeset | files
Fri, 03 Dec 2010 22:40:26 +0100 haftmann merged changeset | files
Fri, 03 Dec 2010 14:46:58 +0100 haftmann conventional point-free characterization of rsp_fold changeset | files
Fri, 03 Dec 2010 14:39:15 +0100 haftmann replaced memb by existing List.member changeset | files
Fri, 03 Dec 2010 14:22:24 +0100 haftmann explicit type constraint; changeset | files
Fri, 03 Dec 2010 22:39:34 +0100 haftmann tuned proposition changeset | files
Fri, 03 Dec 2010 22:34:20 +0100 haftmann lemma multiset_of_rev changeset | files
Fri, 03 Dec 2010 22:34:20 +0100 haftmann lemmas fold_remove1_split and fold_multiset_equiv changeset | files
Fri, 03 Dec 2010 22:08:14 +0100 wenzelm minor tuning for release; changeset | files
Fri, 03 Dec 2010 21:34:54 +0100 wenzelm source files are always encoded as UTF-8; changeset | files
Fri, 03 Dec 2010 21:30:41 +0100 wenzelm eliminated fragile HTML.with_charset -- always use utf-8; changeset | files
Fri, 03 Dec 2010 20:38:58 +0100 wenzelm recoded latin1 as utf8; changeset | files
Fri, 03 Dec 2010 20:26:57 +0100 wenzelm removed old generated stuff; changeset | files
Fri, 03 Dec 2010 20:02:57 +0100 wenzelm comment; changeset | files
Fri, 03 Dec 2010 18:29:49 +0100 blanchet update documentation changeset | files
Fri, 03 Dec 2010 18:29:14 +0100 blanchet replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us changeset | files
Fri, 03 Dec 2010 18:27:21 +0100 blanchet export more information about available SMT solvers changeset | files
Fri, 03 Dec 2010 17:59:13 +0100 wenzelm setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option; changeset | files
Thu, 02 Dec 2010 21:48:36 +0100 traytel use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .." changeset | files
Fri, 03 Dec 2010 17:31:27 +0100 wenzelm updated generated file; changeset | files
Fri, 03 Dec 2010 17:29:27 +0100 wenzelm removed confusing comments (cf. 500171e7aa59); changeset | files
Fri, 03 Dec 2010 17:18:41 +0100 wenzelm merged changeset | files
Fri, 03 Dec 2010 14:00:55 +0100 haftmann removed outdated lint script changeset | files
Fri, 03 Dec 2010 10:43:09 +0100 blanchet merged changeset | files
Fri, 03 Dec 2010 10:28:39 +0100 blanchet compile changeset | files
Fri, 03 Dec 2010 09:55:45 +0100 blanchet run synchronous Auto Tools in parallel changeset | files
Fri, 03 Dec 2010 10:17:55 +0100 krauss really fixed comment (cf. 7abeb749ae99) changeset | files
Fri, 03 Dec 2010 10:03:13 +0100 huffman theorem names generated by the (rep_)datatype command now have mandatory qualifiers changeset | files
Fri, 03 Dec 2010 10:03:10 +0100 krauss eliminated unqualified accesses of datatype facts -- it seems like they all of them were unintended changeset | files
Fri, 03 Dec 2010 09:58:32 +0100 bulwahn NEWS changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn only instantiate type variable if there exists some in quickcheck changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn fixing comment in library changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn adapting predicate_compile_quickcheck changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn adding a nice definition of Id_on for quickcheck and nitpick changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn adding code equation for finiteness of finite types changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn improving sledgehammer_tactic and adding relevance filtering to the tactic changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn adapting mutabelle changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn adapting SML_Quickcheck to recent changes changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn explaining quickcheck testers in the documentation changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn adapting quickcheck examples changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn improving presentation of quickcheck reports changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn declaring quickcheck testers as default after their setup changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn activating construction of exhaustive testing combinators changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn renamed generator into exhaustive changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn checking if parameter is name of a tester which allows e.g. quickcheck[random] changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn moving iteration of tests to the testers in quickcheck changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn removed dead test_term_small function in quickcheck changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn renamed parameter from generator to tester; quickcheck only applies one tester on invocation changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn adding configuration quickcheck_tester changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn adding smart quantifiers to exhaustive testing changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn adapting mutabelle changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn only handle TimeOut exception if used interactively changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn removed interrupt handling that violates Isabelle/ML exception model changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn corrected indentation changeset | files
Fri, 03 Dec 2010 08:40:47 +0100 bulwahn tuned changeset | files
Fri, 03 Dec 2010 08:40:46 +0100 bulwahn smallvalue_generator are defined quick via oracle or sound via function package changeset | files
Fri, 03 Dec 2010 08:40:46 +0100 bulwahn adding shorter output syntax for the finite types of quickcheck changeset | files
Fri, 03 Dec 2010 08:40:46 +0100 bulwahn improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package changeset | files
Fri, 03 Dec 2010 08:40:46 +0100 bulwahn changed order of lemmas to overwrite the general code equation with the nbe-specific one changeset | files
Fri, 03 Dec 2010 00:36:01 +0100 hoelzl adapt proofs to changed set_plus_image (cf. ee8d0548c148); changeset | files
Fri, 03 Dec 2010 17:16:53 +0100 wenzelm bash wrapper: terminate only in exceptional case, keep background processes running (e.g. 'thy_deps' or 'display_drafts'); changeset | files
Fri, 03 Dec 2010 16:39:07 +0100 wenzelm updated latex dependencies (cf. 7d88ebdce380); changeset | files
Fri, 03 Dec 2010 11:21:17 +0100 wenzelm tuned README; changeset | files
Thu, 02 Dec 2010 23:09:54 +0100 wenzelm isabellesym.sty: eliminated dependency on latin1, to allow documents using utf8 instead; changeset | files
Thu, 02 Dec 2010 21:23:56 +0100 wenzelm proper theory name (cf. e84f82418e09); changeset | files
Thu, 02 Dec 2010 21:04:20 +0100 wenzelm merged; changeset | files
Thu, 02 Dec 2010 11:18:44 -0800 huffman merged changeset | files
Wed, 01 Dec 2010 20:52:16 -0800 huffman tuned cpodef code changeset | files
Wed, 01 Dec 2010 20:29:39 -0800 huffman reformulate lemma preorder.ex_ideal, and use it for typedefs changeset | files
Thu, 02 Dec 2010 16:45:28 +0100 hoelzl Prove rel_interior_convex_hull_union (by Grechuck Bogdan). changeset | files
Thu, 02 Dec 2010 16:39:15 +0100 haftmann merged changeset | files
Thu, 02 Dec 2010 16:39:07 +0100 haftmann adapted expected value to more idiomatic numeral representation changeset | files
Thu, 02 Dec 2010 14:34:38 +0100 haftmann corrected representation for code_numeral numerals changeset | files
Thu, 02 Dec 2010 13:53:36 +0100 haftmann separate term_of function for integers -- more canonical representation of negative integers changeset | files
Thu, 02 Dec 2010 16:17:01 +0100 hoelzl merged changeset | files
Thu, 02 Dec 2010 16:16:18 +0100 hoelzl Use coercions in Approximation (by Dmitriy Traytel). changeset | files
Thu, 02 Dec 2010 17:20:34 +0100 wenzelm more antiquotations; changeset | files
Thu, 02 Dec 2010 16:52:52 +0100 wenzelm configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning; changeset | files
Thu, 02 Dec 2010 16:04:22 +0100 wenzelm renamed trace_simp to simp_trace, and debug_simp to simp_debug; changeset | files
Thu, 02 Dec 2010 15:37:32 +0100 wenzelm merged changeset | files
Thu, 02 Dec 2010 15:32:48 +0100 hoelzl merged changeset | files
Thu, 02 Dec 2010 15:09:02 +0100 hoelzl generalized simple_functionD changeset | files
Thu, 02 Dec 2010 14:57:50 +0100 hoelzl Moved theorems to appropriate place. changeset | files
Thu, 02 Dec 2010 14:57:21 +0100 hoelzl Shorter definition for positive_integral. changeset | files
Thu, 02 Dec 2010 14:34:58 +0100 hoelzl Move SUP_commute, SUP_less_iff to HOL image; changeset | files
Wed, 01 Dec 2010 21:03:02 +0100 hoelzl Generalized simple_functionD and less_SUP_iff. changeset | files
Wed, 01 Dec 2010 20:12:53 +0100 hoelzl Tuned setup for borel_measurable with min, max and psuminf. changeset | files
Wed, 01 Dec 2010 20:09:41 +0100 hoelzl Replace algebra_eqI by algebra.equality; changeset | files
Thu, 02 Dec 2010 14:56:16 +0100 blanchet give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def) changeset | files
Thu, 02 Dec 2010 15:03:21 +0100 wenzelm merged changeset | files
Thu, 02 Dec 2010 08:34:23 +0100 nipkow coercions changeset | files
Wed, 01 Dec 2010 20:59:40 +0100 nipkow merged changeset | files
Wed, 01 Dec 2010 20:59:29 +0100 nipkow moved activation of coercion inference into RealDef and declared function real a coercion. changeset | files
Wed, 01 Dec 2010 19:42:09 +0100 hoelzl Corrected IsaMakefile changeset | files
Wed, 01 Dec 2010 19:36:05 +0100 hoelzl merged changeset | files
Wed, 01 Dec 2010 19:33:49 +0100 hoelzl Updated NEWS changeset | files
Wed, 01 Dec 2010 19:27:53 +0100 hoelzl More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability. changeset | files
Wed, 01 Dec 2010 19:20:30 +0100 hoelzl Support product spaces on sigma finite measures. changeset | files
Wed, 01 Dec 2010 18:00:40 +0100 haftmann merged changeset | files
Wed, 01 Dec 2010 15:46:27 +0100 haftmann use type constructor as name for variable changeset | files
Wed, 01 Dec 2010 11:46:20 +0100 haftmann optional explicit prefix for type mapper theorems changeset | files
Wed, 01 Dec 2010 11:33:17 +0100 haftmann file for package tool type_mapper carries the same name as its Isar command changeset | files
Wed, 01 Dec 2010 06:50:54 -0800 huffman merged changeset | files
Wed, 01 Dec 2010 06:48:40 -0800 huffman domain package generates non-authentic syntax rules for parsing only changeset | files
Thu, 02 Dec 2010 10:46:03 +0100 wenzelm builtin time bounds (again); changeset | files
Thu, 02 Dec 2010 10:44:33 +0100 wenzelm tuned; changeset | files
Wed, 01 Dec 2010 21:23:21 +0100 wenzelm more abstract handling of Time properties; changeset | files
Wed, 01 Dec 2010 21:07:50 +0100 wenzelm store tooltip-dismiss-delay as Double(seconds); changeset | files
Wed, 01 Dec 2010 20:34:40 +0100 wenzelm more abstract/uniform handling of time, preferring seconds as Double; changeset | files
Wed, 01 Dec 2010 15:38:05 +0100 wenzelm merged changeset | files
Wed, 01 Dec 2010 11:45:37 +0100 haftmann NEWS changeset | files
Wed, 01 Dec 2010 15:35:40 +0100 wenzelm just one HOLogic.mk_comp; changeset | files
Wed, 01 Dec 2010 15:03:44 +0100 wenzelm more direct use of binder_types/body_type; changeset | files
Wed, 01 Dec 2010 15:02:39 +0100 wenzelm tuned; changeset | files
Wed, 01 Dec 2010 14:56:07 +0100 wenzelm simplified HOL.eq simproc matching; changeset | files
Wed, 01 Dec 2010 13:37:31 +0100 wenzelm tuned; changeset | files
Wed, 01 Dec 2010 13:09:08 +0100 wenzelm just one Term.dest_funT; changeset | files
Wed, 01 Dec 2010 11:32:24 +0100 wenzelm activate subtyping/coercions in theory Complex_Main; changeset | files
Wed, 01 Dec 2010 11:06:01 +0100 wenzelm simplified equality on pairs of types; changeset | files
Wed, 01 Dec 2010 11:01:20 +0100 wenzelm more precise dependencies; changeset | files
Mon, 29 Nov 2010 16:53:08 +0100 traytel two-staged architecture for subtyping; changeset | files
Tue, 30 Nov 2010 20:02:01 -0800 huffman merged changeset | files
Tue, 30 Nov 2010 15:56:19 -0800 huffman change cpodef-generated cont_Rep rules to cont2cont format changeset | files
Tue, 30 Nov 2010 15:34:51 -0800 huffman internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules changeset | files
Tue, 30 Nov 2010 14:21:57 -0800 huffman remove gratuitous semicolons from ML code changeset | files
Tue, 30 Nov 2010 14:01:49 -0800 huffman add continuity lemma for List.map changeset | files
Tue, 30 Nov 2010 14:01:25 -0800 huffman simplify predomain instances changeset | files
Tue, 30 Nov 2010 21:54:15 +0100 boehmes merged changeset | files
Tue, 30 Nov 2010 18:22:43 +0100 boehmes split up Z3 models into constraints on free variables and constant definitions; changeset | files
Tue, 30 Nov 2010 20:52:49 +0100 haftmann code preprocessor setup for numerals on word type; changeset | files
Tue, 30 Nov 2010 18:40:23 +0100 haftmann merged changeset | files
Tue, 30 Nov 2010 17:22:59 +0100 haftmann adaptions to changes in Equiv_Relation.thy changeset | files
Tue, 30 Nov 2010 17:19:11 +0100 haftmann adapted fragile proof changeset | files
Tue, 30 Nov 2010 17:19:11 +0100 haftmann adaptions to changes in Equiv_Relation.thy; prefer primrec if possible changeset | files
Tue, 30 Nov 2010 17:19:11 +0100 haftmann adaptions to changes in Equiv_Relation.thy changeset | files
Tue, 30 Nov 2010 15:58:21 +0100 haftmann merged changeset | files
Tue, 30 Nov 2010 15:58:09 +0100 haftmann more systematic and compact proofs on type relation operators using natural deduction rules changeset | files
Tue, 30 Nov 2010 15:58:09 +0100 haftmann adapted proofs to slightly changed definitions of congruent(2) changeset | files
Mon, 29 Nov 2010 22:47:55 +0100 haftmann reorienting iff in Quotient_rel prevents simplifier looping; changeset | files
Mon, 29 Nov 2010 22:41:17 +0100 haftmann replaced slightly odd locale congruent2 by plain definition changeset | files
Mon, 29 Nov 2010 22:32:06 +0100 haftmann replaced slightly odd locale congruent by plain definition changeset | files
Mon, 29 Nov 2010 13:44:54 +0100 haftmann equivI has replaced equiv.intro changeset | files
Mon, 29 Nov 2010 12:15:14 +0100 haftmann moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; changeset | files
Mon, 29 Nov 2010 12:14:46 +0100 haftmann moved generic definitions about relations from Quotient.thy to Predicate; changeset | files
Mon, 29 Nov 2010 12:14:43 +0100 haftmann moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; changeset | files
Tue, 30 Nov 2010 08:58:47 -0800 huffman simplify proof of LIMSEQ_unique changeset | files
Tue, 30 Nov 2010 08:35:04 -0800 huffman use new 'file' antiquotation for reference to Dedekind_Real.thy changeset | files
Tue, 30 Nov 2010 08:00:50 -0800 huffman merged changeset | files
Mon, 29 Nov 2010 14:37:40 -0800 huffman instance list :: (discrete_cpo) discrete_cpo; changeset | files
Tue, 30 Nov 2010 00:12:29 +0100 boehmes merged changeset | files
Mon, 29 Nov 2010 23:41:09 +0100 boehmes also support higher-order rules for Z3 proof reconstruction changeset | files
Mon, 29 Nov 2010 16:10:44 +0100 wenzelm merged changeset | files
Mon, 29 Nov 2010 11:39:00 +0100 haftmann less ghc-specific pragma changeset | files
Mon, 29 Nov 2010 11:38:59 +0100 haftmann tuned changeset | files
Mon, 29 Nov 2010 11:27:39 +0100 wenzelm updated generated files; changeset | files
Mon, 29 Nov 2010 11:22:40 +0100 wenzelm added document antiquotation @{file}; changeset | files
Sun, 28 Nov 2010 21:07:28 +0100 wenzelm Parse.liberal_name for document antiquotations and attributes; changeset | files
Sun, 28 Nov 2010 20:36:45 +0100 wenzelm ML results: enter before printing (cf. Poly/ML SVN 1218); changeset | files
Sun, 28 Nov 2010 20:12:22 +0100 wenzelm merged changeset | files
Sun, 28 Nov 2010 08:41:16 -0800 huffman merged changeset | files
Sun, 28 Nov 2010 08:21:52 -0800 huffman merged changeset | files
Sun, 28 Nov 2010 07:29:32 -0800 huffman change match_bottom_simps to produce if-then-else, making more uses of bottom-patterns work with fixrec changeset | files
Sat, 27 Nov 2010 22:48:08 -0800 huffman add lemma cont2cont_if_bottom changeset | files
Sun, 28 Nov 2010 20:03:19 +0100 wenzelm added Parse.literal_fact with proper inner_syntax markup (source position); changeset | files
Sun, 28 Nov 2010 19:35:14 +0100 wenzelm tuned signature; changeset | files
Sun, 28 Nov 2010 19:30:52 +0100 wenzelm less frequent sidekick parsing, which is relatively slow; changeset | files
Sun, 28 Nov 2010 18:31:54 +0100 wenzelm basic setup for bundled Java runtime; changeset | files
Sun, 28 Nov 2010 17:58:38 +0100 wenzelm updated reference platforms; changeset | files
Sun, 28 Nov 2010 16:42:54 +0100 wenzelm merged changeset | files
Sun, 28 Nov 2010 15:21:02 +0100 nipkow merged changeset | files
Sun, 28 Nov 2010 15:20:51 +0100 nipkow gave more standard finite set rules simp and intro attribute changeset | files
Sun, 28 Nov 2010 16:35:56 +0100 wenzelm more permissive Isabelle_System.mkdir; changeset | files
Sun, 28 Nov 2010 16:15:31 +0100 wenzelm added 'syntax_declaration' command; changeset | files
Sun, 28 Nov 2010 15:34:35 +0100 wenzelm more conventional exception propagation -- taking into account Simple_Thread.fork wrapping; changeset | files
Sun, 28 Nov 2010 15:28:48 +0100 wenzelm superficial tuning; changeset | files
Sun, 28 Nov 2010 14:01:20 +0100 wenzelm updated versions; changeset | files
Sun, 28 Nov 2010 13:58:29 +0100 wenzelm recovered Isabelle2009-2 NEWS -- published part is read-only; changeset | files
Sun, 28 Nov 2010 13:55:19 +0100 wenzelm follow-up to HOLCF move (cf. 0437dbc127b3, 04d44a20fccf); changeset | files
Sun, 28 Nov 2010 12:11:41 +0100 krauss removed HOLCF for now as explicit component changeset | files
Sat, 27 Nov 2010 17:44:36 -0800 huffman fix cut-and-paste errors for HOLCF entries in IsaMakefile changeset | files
Sat, 27 Nov 2010 17:29:21 -0800 huffman update web description of HOLCF; changeset | files
Sat, 27 Nov 2010 17:14:29 -0800 huffman remove HOLCF from build script, since it no longer works changeset | files
Sat, 27 Nov 2010 16:08:10 -0800 huffman moved directory src/HOLCF to src/HOL/HOLCF; changeset | files
Sat, 27 Nov 2010 14:34:54 -0800 huffman merged changeset | files
Sat, 27 Nov 2010 14:09:03 -0800 huffman rename Pcpodef.thy to Cpodef.thy; changeset | files
Sat, 27 Nov 2010 13:12:10 -0800 huffman renamed several HOLCF theorems (listed in NEWS) changeset | files
Sat, 27 Nov 2010 12:55:12 -0800 huffman rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo changeset | files
Sat, 27 Nov 2010 12:38:02 -0800 huffman rename rep_contlub lemmas to rep_lub changeset | files
Sat, 27 Nov 2010 12:27:57 -0800 huffman rename function 'match_UU' to 'match_bottom' changeset | files
Sat, 27 Nov 2010 12:26:18 -0800 huffman rename function 'strict' to 'seq', which is its name in Haskell changeset | files
Sat, 27 Nov 2010 22:02:16 +0100 haftmann merged changeset | files
Sat, 27 Nov 2010 22:01:45 +0100 haftmann merged changeset | files
Sat, 27 Nov 2010 22:01:27 +0100 haftmann typscheme with signatures is inappropriate when building empty certificate; changeset | files
Sat, 27 Nov 2010 19:42:41 +0100 haftmann merged changeset | files
Sat, 27 Nov 2010 19:41:37 +0100 haftmann merged changeset | files
Sat, 27 Nov 2010 19:41:28 +0100 haftmann corrected: use canonical variables of type scheme uniformly changeset | files
Sat, 27 Nov 2010 19:41:27 +0100 haftmann tuned changeset | files
Fri, 26 Nov 2010 23:50:14 +0100 haftmann merged changeset | files
Fri, 26 Nov 2010 23:49:49 +0100 haftmann consider sort constraints for datatype constructors when constructing the empty equation certificate; changeset | files
Fri, 26 Nov 2010 23:49:49 +0100 haftmann tuned example changeset | files
Sat, 27 Nov 2010 20:48:06 +0100 wenzelm merged changeset | files
Sat, 27 Nov 2010 18:51:15 +0100 haftmann updated generated documents changeset | files
Sat, 27 Nov 2010 18:51:04 +0100 haftmann added equation for Queue; changeset | files
Sat, 27 Nov 2010 18:51:04 +0100 haftmann added evaluation section changeset | files
Sat, 27 Nov 2010 18:51:04 +0100 haftmann tuned formatting; changeset | files
Sat, 27 Nov 2010 18:51:04 +0100 haftmann added label changeset | files
Sat, 27 Nov 2010 20:10:57 +0100 wenzelm more thorough process termination (cf. Scala version); changeset | files
Sat, 27 Nov 2010 19:17:55 +0100 wenzelm prefer Isabelle/ML concurrency elements; changeset | files
Sat, 27 Nov 2010 16:29:53 +0100 wenzelm removed bash from ML system bootstrap, and past the Secure ML barrier; changeset | files
Sat, 27 Nov 2010 16:27:52 +0100 wenzelm more proper int wrappers; changeset | files
Sat, 27 Nov 2010 15:58:36 +0100 wenzelm explicit check for requirement; changeset | files
Sat, 27 Nov 2010 15:45:20 +0100 wenzelm more basic Isabelle_System.mkdir; changeset | files
Sat, 27 Nov 2010 15:36:35 +0100 wenzelm tuned; changeset | files
Sat, 27 Nov 2010 15:28:00 +0100 wenzelm more explicit Isabelle_System operations; changeset | files
Sat, 27 Nov 2010 14:32:08 +0100 wenzelm prefer Synchronized.var over CRITICAL/Unsynchronized.ref; changeset | files
Sat, 27 Nov 2010 14:19:04 +0100 wenzelm moved file identification to thy_load.ML (where it is actually used); changeset | files
Sat, 27 Nov 2010 12:02:19 +0100 wenzelm removed some old settings; changeset | files
Sat, 27 Nov 2010 11:51:05 +0100 wenzelm recovered global "Isabelle" symlink for isatest (cf. 7f745e4b7cce); changeset | files
Fri, 26 Nov 2010 15:49:59 -0800 huffman merged changeset | files
Fri, 26 Nov 2010 15:24:11 -0800 huffman remove map function names from domain package theory data changeset | files
Fri, 26 Nov 2010 14:13:34 -0800 huffman isar-style proof for lemma contI2 changeset | files
Fri, 26 Nov 2010 15:11:08 -0800 huffman remove case combinator for fixrec match type changeset | files
Fri, 26 Nov 2010 14:10:34 -0800 huffman declare more simp rules for powerdomains changeset | files
Sat, 27 Nov 2010 00:00:54 +0100 wenzelm merged; changeset | files
Fri, 26 Nov 2010 23:14:14 +0100 haftmann merged changeset | files
Fri, 26 Nov 2010 23:13:58 +0100 haftmann strict forall2 changeset | files
Fri, 26 Nov 2010 23:13:58 +0100 haftmann nbe decides equality of abstractions by extensionality changeset | files
Fri, 26 Nov 2010 23:51:34 +0100 wenzelm eliminated some generated comments; changeset | files
Fri, 26 Nov 2010 23:41:23 +0100 wenzelm merged changeset | files
Fri, 26 Nov 2010 23:12:01 +0100 haftmann merged changeset | files
Fri, 26 Nov 2010 22:33:21 +0100 haftmann keep type variable arguments of datatype constructors in bookkeeping changeset | files
Fri, 26 Nov 2010 22:36:55 +0100 blanchet document changes in Nitpick and MESON/Metis changeset | files
Fri, 26 Nov 2010 22:36:24 +0100 blanchet renamed "trace_me{son,tis}" and "verbose_metis" to have the name of the tool first changeset | files
Fri, 26 Nov 2010 22:22:07 +0100 blanchet put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs changeset | files
Fri, 26 Nov 2010 22:29:41 +0100 wenzelm make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths; changeset | files
Fri, 26 Nov 2010 22:04:33 +0100 wenzelm just one version of fold_rev2; changeset | files
Fri, 26 Nov 2010 21:31:46 +0100 wenzelm explicit use of unprefix; changeset | files
Fri, 26 Nov 2010 21:09:36 +0100 wenzelm keep private things private, without comments; changeset | files
Fri, 26 Nov 2010 20:52:21 +0100 wenzelm eliminated some clones of eq_list; changeset | files
Fri, 26 Nov 2010 18:07:00 +0100 nipkow merged changeset | files
Fri, 26 Nov 2010 18:06:48 +0100 nipkow new lemma changeset | files
Fri, 26 Nov 2010 17:54:15 +0100 wenzelm lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately; changeset | files
Fri, 26 Nov 2010 16:28:34 +0100 wenzelm prefer non-classical eliminations in Pure reasoning, notably "rule" steps; changeset | files
Fri, 26 Nov 2010 14:40:33 +0100 wenzelm discontinued global "Isabelle" symlink, to make each distribution even more self-contained; changeset | files
Fri, 26 Nov 2010 14:19:16 +0100 wenzelm more correct spelling; changeset | files
Fri, 26 Nov 2010 12:03:18 +0100 haftmann globbing constant expressions use more idiomatic underscore rather than star changeset | files
Fri, 26 Nov 2010 12:03:17 +0100 haftmann globbing constant expressions use more idiomatic underscore rather than star; changeset | files
Fri, 26 Nov 2010 11:38:20 +0100 haftmann datatype constructor glob for code_reflect changeset | files
Fri, 26 Nov 2010 11:06:49 +0100 haftmann merged changeset | files
Fri, 26 Nov 2010 09:32:26 +0100 haftmann merged changeset | files
Thu, 25 Nov 2010 15:40:41 +0100 haftmann merged changeset | files
Thu, 25 Nov 2010 15:40:15 +0100 haftmann toplevel deresolving for flat module name space changeset | files
Fri, 26 Nov 2010 10:04:04 +0100 hoelzl merged changeset | files
Tue, 23 Nov 2010 14:14:17 +0100 hoelzl Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image. changeset | files
Mon, 22 Nov 2010 10:34:33 +0100 hoelzl Replace surj by abbreviation; remove surj_on. changeset | files
Fri, 26 Nov 2010 09:15:49 +0100 blanchet adjust Sledgehammer/SMT fudge factor changeset | files
Thu, 25 Nov 2010 16:12:23 +0100 wenzelm clarified Par_List.managed_results, with explicit propagation of outermost physical interrupt to forked futures (e.g. to make timeout apply here as expected and prevent zombies); changeset | files
Thu, 25 Nov 2010 14:59:01 +0100 blanchet merge changeset | files
Thu, 25 Nov 2010 14:58:50 +0100 blanchet cosmetics changeset | files
Thu, 25 Nov 2010 14:58:20 +0100 blanchet eta-reduce on the fly to prevent an exception changeset | files
Thu, 25 Nov 2010 14:36:51 +0100 nipkow merged changeset | files
Thu, 25 Nov 2010 14:35:52 +0100 nipkow Added the simplest finite Ramsey theorem changeset | files
Thu, 25 Nov 2010 14:13:48 +0100 blanchet reverted c059d550afec -- the triviality check had apparently nothing to do with spontaneous Interrupt exceptions changeset | files
Thu, 25 Nov 2010 13:26:12 +0100 blanchet set Metis option on correct context, lest it be ignored changeset | files
Thu, 25 Nov 2010 12:11:12 +0100 blanchet make "debug" mode of Sledgehammer/SMT more liberal changeset | files
Thu, 25 Nov 2010 00:32:30 +0100 blanchet fix check for builtinness of 0 and 1 -- these aren't functions changeset | files
Thu, 25 Nov 2010 00:17:16 +0100 blanchet added "no_atp" for fact that confuses the SMT normalizer and that doesn't help ATPs anyway changeset | files
Wed, 24 Nov 2010 23:17:24 +0100 blanchet document requirement on theory import changeset | files
Wed, 24 Nov 2010 19:15:00 +0100 haftmann corrected abd4e7358847 where SOMEthing went utterly wrong changeset | files
Wed, 24 Nov 2010 16:51:13 +0100 boehmes merged changeset | files
Wed, 24 Nov 2010 15:33:35 +0100 boehmes swap names for built-in tester functions (to better reflect the intuition of what they do); changeset | files
Wed, 24 Nov 2010 13:31:12 +0100 boehmes instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers) changeset | files
Wed, 24 Nov 2010 16:15:15 +0100 blanchet more precise error handling in Sledgehammer/SMT for Z3 and remote SMT provers changeset | files
Wed, 24 Nov 2010 10:52:02 +0100 bulwahn removing Enum.in_enum from the claset changeset | files
Wed, 24 Nov 2010 10:42:28 +0100 boehmes merged changeset | files
Wed, 24 Nov 2010 10:39:58 +0100 boehmes be more precise: only treat constant 'distinct' applied to an explicit list as built-in changeset | files
Wed, 24 Nov 2010 08:51:48 +0100 boehmes be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed) changeset | files
Wed, 24 Nov 2010 10:23:52 +0100 bulwahn announcing some latest change (d40b347d5b0b) changeset | files
Tue, 23 Nov 2010 23:44:11 +0100 blanchet merged changeset | files
Tue, 23 Nov 2010 23:43:56 +0100 blanchet more precise characterization of built-in constants "number_of", "0", and "1" changeset | files
Tue, 23 Nov 2010 23:11:06 +0100 haftmann merged changeset | files
Mon, 22 Nov 2010 17:49:24 +0100 haftmann merged changeset | files
Mon, 22 Nov 2010 17:48:35 +0100 haftmann adhere established Collect/mem convention more closely changeset | files
Mon, 22 Nov 2010 17:49:12 +0100 haftmann merged changeset | files
Mon, 22 Nov 2010 17:46:51 +0100 haftmann replaced misleading Fset/fset name -- these do not stand for finite sets changeset | files
Mon, 22 Nov 2010 09:37:39 +0100 haftmann renamed slightly ambivalent crel to effect changeset | files
Tue, 23 Nov 2010 23:10:13 +0100 blanchet disable triviality checking -- it might be the source of the spurious Interrupt exceptions that make it almost impossible to run Judgement Day changeset | files
Tue, 23 Nov 2010 22:37:16 +0100 blanchet more precise error handling for Z3; changeset | files
Tue, 23 Nov 2010 21:54:03 +0100 blanchet use "Thm.transfer" in Sledgehammer to prevent theory merger issues in "SMT_Solver.smt_filter" later on changeset | files
Tue, 23 Nov 2010 19:01:21 +0100 blanchet make Mirabelle take into consideration whether the SMT solver proof should be reconstructed with Metis or SMT changeset | files
Tue, 23 Nov 2010 18:28:09 +0100 blanchet try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates changeset | files
Tue, 23 Nov 2010 18:26:56 +0100 blanchet added "verbose" option to Metis to shut up its warnings if necessary changeset | files
Mon, 22 Nov 2010 23:37:00 +0100 boehmes added support for quantifier weight annotations changeset | files
Mon, 22 Nov 2010 15:45:43 +0100 boehmes share and use more utility functions; changeset | files
Mon, 22 Nov 2010 15:45:42 +0100 boehmes added prove reconstruction for injective functions; changeset | files
Mon, 22 Nov 2010 14:27:42 +0100 haftmann generous timeout gives more breath in parallel run on less luxury machines changeset | files
Mon, 22 Nov 2010 14:19:03 +0100 bulwahn adding setup for exhaustive testing in example file changeset | files
Mon, 22 Nov 2010 11:35:11 +0100 bulwahn hiding enum changeset | files
Mon, 22 Nov 2010 11:35:09 +0100 bulwahn adapting example in Predicate_Compile_Examples changeset | files
Mon, 22 Nov 2010 11:35:07 +0100 bulwahn hiding the constants changeset | files
Mon, 22 Nov 2010 11:35:06 +0100 bulwahn improving function is_iterable in quickcheck changeset | files
Mon, 22 Nov 2010 11:35:02 +0100 bulwahn adding temporary options to the quickcheck examples changeset | files
Mon, 22 Nov 2010 11:35:00 +0100 bulwahn adapting the quickcheck examples changeset | files
Mon, 22 Nov 2010 11:34:59 +0100 bulwahn adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle changeset | files
Mon, 22 Nov 2010 11:34:58 +0100 bulwahn adding code equations for EX1 on finite types changeset | files
Mon, 22 Nov 2010 11:34:57 +0100 bulwahn adding code equation for function equality; adding some instantiations for the finite types changeset | files
Mon, 22 Nov 2010 11:34:56 +0100 bulwahn adding Enum to HOL-Main image and removing it from HOL-Library changeset | files
Mon, 22 Nov 2010 11:34:55 +0100 bulwahn moving Enum theory from HOL/Library to HOL changeset | files
Mon, 22 Nov 2010 11:34:54 +0100 bulwahn splitting test_goal function in two functions; exporting new configurations in quickcheck; iterations depend on generator_name in quickcheck changeset | files
Mon, 22 Nov 2010 11:34:53 +0100 bulwahn adding prototype for finite_type instantiations changeset | files
Mon, 22 Nov 2010 11:34:52 +0100 bulwahn adding option finite_types to quickcheck changeset | files
Mon, 22 Nov 2010 11:34:50 +0100 bulwahn adding test cases for smallcheck and adding examples where exhaustive testing is more successful changeset | files
Mon, 22 Nov 2010 10:42:07 +0100 bulwahn changed old-style quickcheck configurations to new Config.T configurations changeset | files
Mon, 22 Nov 2010 10:42:06 +0100 bulwahn adding temporary function test_test_small to Quickcheck changeset | files
Mon, 22 Nov 2010 10:42:04 +0100 bulwahn added useful function map_context_result to signature changeset | files
Mon, 22 Nov 2010 10:42:03 +0100 bulwahn moving the error handling to the right scope in smallvalue_generators changeset | files
Mon, 22 Nov 2010 10:42:01 +0100 bulwahn removing clone from function package and using the clean interface from Function_Relation instead changeset | files
Mon, 22 Nov 2010 10:41:58 +0100 bulwahn adding function generation to SmallCheck; activating exhaustive search space testing changeset | files
Mon, 22 Nov 2010 10:41:57 +0100 bulwahn adding dummy definition for Code_Evaluation.Abs and hiding constants App less strict changeset | files
Mon, 22 Nov 2010 10:41:56 +0100 bulwahn generalized ensure_random_datatype to ensure_sort_datatype changeset | files
Mon, 22 Nov 2010 10:41:56 +0100 bulwahn renaming quickcheck generator code to random changeset | files
Mon, 22 Nov 2010 10:41:55 +0100 bulwahn ported sledgehammer_tactic to current development version changeset | files
Mon, 22 Nov 2010 10:41:54 +0100 bulwahn adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test changeset | files
Mon, 22 Nov 2010 10:41:53 +0100 bulwahn adding files to use sledgehammer as a tactic for non-interactive use changeset | files
Mon, 22 Nov 2010 10:41:52 +0100 bulwahn adding birthday paradoxon from some abandoned drawer changeset | files
Mon, 22 Nov 2010 10:41:51 +0100 bulwahn adding extensional function spaces to the FuncSet library theory changeset | files
Mon, 22 Nov 2010 09:19:34 +0100 haftmann tuned changeset | files
Mon, 22 Nov 2010 09:18:25 +0100 haftmann tuned changeset | files
Sat, 20 Nov 2010 01:07:16 +0100 wenzelm updated explode vs. raw_explode; changeset | files
Sat, 20 Nov 2010 00:53:26 +0100 wenzelm renamed raw "explode" function to "raw_explode" to emphasize its meaning; changeset | files
Fri, 19 Nov 2010 23:48:07 +0100 wenzelm total Symbol.explode (cf. 1050315f6ee2); changeset | files
Fri, 19 Nov 2010 21:14:12 +0100 wenzelm do not export Thy_Load.required, to avoid confusion about the interface; changeset | files
Fri, 19 Nov 2010 09:07:23 -0800 huffman merged changeset | files
Wed, 17 Nov 2010 16:13:33 -0800 huffman declare adm_chfin [simp] changeset | files
Wed, 17 Nov 2010 16:05:18 -0800 huffman add lemma cont_fun; remove unused lemma monofun_app changeset | files
Wed, 17 Nov 2010 12:19:19 -0800 huffman accumulated NEWS updates for HOLCF changeset | files
Wed, 17 Nov 2010 11:39:44 -0800 huffman section -> subsection changeset | files
Wed, 17 Nov 2010 11:07:02 -0800 huffman add lemma adm_prod_case changeset | files
Fri, 19 Nov 2010 14:59:11 +0000 paulson merged changeset | files
Fri, 19 Nov 2010 14:58:49 +0000 paulson First-order pattern matching: catch a rogue exception (differing numbers of arguments) changeset | files
Fri, 19 Nov 2010 14:35:58 +0100 haftmann eval simp rules for predicate type, simplify primitive proofs changeset | files
Fri, 19 Nov 2010 11:44:46 +0100 haftmann generalized type changeset | files
Fri, 19 Nov 2010 10:37:06 +0100 haftmann made smlnj happy changeset | files
Fri, 19 Nov 2010 10:04:08 +0100 haftmann merged changeset | files
Thu, 18 Nov 2010 18:53:36 +0100 haftmann proper qualification needed due to shadowing on theory merge changeset | files
Thu, 18 Nov 2010 17:06:02 +0100 haftmann more appropriate name for property changeset | files
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for sum type changeset | files
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for option type changeset | files
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for list type; map_pair replaces prod_fun changeset | files
Thu, 18 Nov 2010 17:01:16 +0100 haftmann map_pair replaces prod_fun changeset | files
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for mulitset type changeset | files
Thu, 18 Nov 2010 17:01:16 +0100 haftmann mapper for mapping type changeset | files
Thu, 18 Nov 2010 17:01:15 +0100 haftmann mapper for fset type changeset | files
Thu, 18 Nov 2010 17:01:15 +0100 haftmann mapper for dlist type changeset | files
Thu, 18 Nov 2010 17:01:15 +0100 haftmann map_fun combinator in theory Fun changeset | files
Thu, 18 Nov 2010 22:34:32 +0100 wenzelm some updates after 2 years of Mercurial usage; changeset | files
Thu, 18 Nov 2010 18:12:03 +0100 blanchet mention Sledgehammer with SMT changeset | files
Thu, 18 Nov 2010 18:09:08 +0100 blanchet enabled SMT solver in Sledgehammer by default changeset | files
Thu, 18 Nov 2010 12:37:30 +0100 haftmann merged changeset | files
Thu, 18 Nov 2010 10:59:42 +0100 haftmann keep variables bound changeset | files
Thu, 18 Nov 2010 10:52:38 +0100 blanchet remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem changeset | files
Wed, 17 Nov 2010 23:20:26 +0100 haftmann merged changeset | files
Wed, 17 Nov 2010 17:27:25 +0100 haftmann infer variances of user-given mapper operation; proper thm storing changeset | files
Wed, 17 Nov 2010 21:35:23 +0100 nipkow code eqn for slice was missing; redefined splice with fun changeset | files
Wed, 17 Nov 2010 08:47:58 -0800 huffman move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain changeset | files
Wed, 17 Nov 2010 06:49:23 -0800 huffman merged changeset | files
Tue, 16 Nov 2010 16:36:57 -0800 huffman typedef (open) unit changeset | files
Tue, 16 Nov 2010 13:37:17 -0800 huffman add bind_bind rules for powerdomains changeset | files
Wed, 17 Nov 2010 13:50:02 +0100 wenzelm merged changeset | files
Wed, 17 Nov 2010 12:24:58 +0100 haftmann emerging Isar command interface changeset | files
Wed, 17 Nov 2010 11:38:47 +0100 haftmann fixed typo changeset | files
Wed, 17 Nov 2010 11:38:46 +0100 haftmann updated keywords changeset | files
Wed, 17 Nov 2010 11:27:48 +0100 haftmann ML signature interface changeset | files
Wed, 17 Nov 2010 11:26:39 +0100 haftmann stub for Isar command interface changeset | files
Wed, 17 Nov 2010 11:09:18 +0100 haftmann module for functorial mappers changeset | files
Wed, 17 Nov 2010 13:39:30 +0100 wenzelm merged changeset | files
Wed, 17 Nov 2010 09:22:23 +0100 boehmes require the b2i file ending in the boogie_open command (for consistency with the theory header) changeset | files
Wed, 17 Nov 2010 08:14:56 +0100 boehmes use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable) changeset | files
Wed, 17 Nov 2010 08:14:55 +0100 boehmes keep input and output files used to communicate with the SMT solver (for debugging purposes mainly) changeset | files
Tue, 16 Nov 2010 12:08:28 -0800 huffman add lemmas about powerdomains changeset | files
Tue, 16 Nov 2010 11:57:10 -0800 huffman declare {upper,lower,convex}_pd_induct as default induction rules changeset | files
Tue, 16 Nov 2010 11:50:05 -0800 huffman rename 'repdef' to 'domaindef' changeset | files
Wed, 17 Nov 2010 13:38:53 +0100 wenzelm refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text; changeset | files
Wed, 17 Nov 2010 11:24:07 +0100 wenzelm less parentheses, cf. Session.welcome; changeset | files
Tue, 16 Nov 2010 22:40:45 +0100 wenzelm avoid spam; changeset | files
Tue, 16 Nov 2010 22:13:54 +0100 wenzelm more robust determination of java executable; changeset | files
Tue, 16 Nov 2010 21:54:52 +0100 wenzelm init_component: require absolute path (when invoked by user scripts); changeset | files
Tue, 16 Nov 2010 21:48:14 +0100 wenzelm more explicit explanation of init_component shell function; changeset | files
Tue, 16 Nov 2010 20:30:25 +0100 wenzelm paranoia export of CLASSPATH, just in case the initial status via allexport is lost due to other scripts; changeset | files
Tue, 16 Nov 2010 17:27:11 +0100 wenzelm tuned message; changeset | files
Tue, 16 Nov 2010 15:29:01 +0100 wenzelm post raw messages last, to ensure that result has been handled by session actor already (e.g. to avoid race between Session.session_actor and Session_Dockable.main_actor); changeset | files
Tue, 16 Nov 2010 15:23:26 +0100 wenzelm more reasonably defaults for typical laptops (2 GB RAM, 2 cores); changeset | files
Tue, 16 Nov 2010 10:33:36 +0100 haftmann added forall2 predicate lifter changeset | files
Mon, 15 Nov 2010 22:31:18 +0100 wenzelm merged changeset | files
Mon, 15 Nov 2010 22:24:08 +0100 boehmes merged changeset | files
Mon, 15 Nov 2010 22:23:28 +0100 boehmes renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed changeset | files
Mon, 15 Nov 2010 22:23:26 +0100 boehmes honour timeouts which are not rounded to full seconds changeset | files
Mon, 15 Nov 2010 22:08:01 +0100 blanchet better error message changeset | files
Mon, 15 Nov 2010 21:08:48 +0100 blanchet better error message changeset | files
Mon, 15 Nov 2010 20:48:48 +0100 wenzelm merged changeset | files
Mon, 15 Nov 2010 18:58:30 +0100 blanchet cosmetics changeset | files
Mon, 15 Nov 2010 18:56:31 +0100 blanchet interpret SMT_Failure.Solver_Crashed correctly changeset | files
Mon, 15 Nov 2010 18:56:30 +0100 blanchet turn on Sledgehammer verbosity so we can track down crashes changeset | files
Mon, 15 Nov 2010 18:56:29 +0100 blanchet pick up SMT solver crashes and report them to the user/Mirabelle if desired changeset | files
Mon, 15 Nov 2010 18:04:04 +0100 boehmes merged changeset | files
Mon, 15 Nov 2010 17:52:48 +0100 boehmes only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers changeset | files
Mon, 15 Nov 2010 17:35:57 +0100 boehmes trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3) changeset | files
Mon, 15 Nov 2010 17:04:53 +0100 bulwahn merged changeset | files
Mon, 15 Nov 2010 13:40:12 +0100 bulwahn ignoring the constant STR in the predicate compiler changeset | files
Mon, 15 Nov 2010 17:40:38 +0100 wenzelm non-executable source files; changeset | files
Mon, 15 Nov 2010 17:39:23 +0100 wenzelm eliminated old-style sed in favour of builtin regex matching; changeset | files
Mon, 15 Nov 2010 17:14:43 +0100 wenzelm more robust treatment of spaces in file names; changeset | files
Mon, 15 Nov 2010 15:41:58 +0100 wenzelm tuned error messages; changeset | files
Mon, 15 Nov 2010 14:59:53 +0100 wenzelm merged changeset | files
Mon, 15 Nov 2010 14:59:21 +0100 haftmann re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10) changeset | files
Mon, 15 Nov 2010 14:14:38 +0100 haftmann re-generalized type of prod_rel (accident from 2989f9f3aa10) changeset | files
Mon, 15 Nov 2010 00:20:36 +0100 boehmes formal dependency on b2i files changeset | files
Sun, 14 Nov 2010 23:55:25 +0100 boehmes merged changeset | files
Fri, 12 Nov 2010 17:28:43 +0100 boehmes check the return code of the SMT solver and raise an exception if the prover failed changeset | files
Sun, 14 Nov 2010 17:33:28 +0100 wenzelm updated README; changeset | files
Sun, 14 Nov 2010 15:25:01 +0100 wenzelm tuned; changeset | files
Sun, 14 Nov 2010 15:21:49 +0100 wenzelm cover 'write' as primitive proof command; changeset | files
Sun, 14 Nov 2010 14:05:08 +0100 wenzelm clarified interact/print state: proof commands are treated as in TTY mode to get full response; changeset | files
Sat, 13 Nov 2010 22:33:07 +0100 wenzelm somewhat adhoc replacement for 'thus' and 'hence'; changeset | files
Sat, 13 Nov 2010 21:46:24 +0100 wenzelm always print state of proof commands (notably "qed" etc.); changeset | files
Sat, 13 Nov 2010 21:01:03 +0100 wenzelm simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing; changeset | files
Sat, 13 Nov 2010 20:49:02 +0100 wenzelm tuned message; changeset | files
Sat, 13 Nov 2010 20:20:05 +0100 wenzelm proper escape in regex; changeset | files
Sat, 13 Nov 2010 20:13:35 +0100 wenzelm report malformed symbols; changeset | files
Sat, 13 Nov 2010 20:06:52 +0100 wenzelm qualified Symbol_Pos.symbol; changeset | files
Sat, 13 Nov 2010 19:55:45 +0100 wenzelm total Symbol.source; changeset | files
Sat, 13 Nov 2010 19:47:23 +0100 wenzelm eliminated slightly odd pervasive Symbol_Pos.symbol; changeset | files
Sat, 13 Nov 2010 19:27:41 +0100 wenzelm treat Unicode "replacement character" (i.e. decoding error) is malformed; changeset | files
Sat, 13 Nov 2010 19:21:53 +0100 wenzelm simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.); changeset | files
Sat, 13 Nov 2010 16:46:00 +0100 wenzelm tuned; changeset | files
Sat, 13 Nov 2010 12:32:21 +0100 wenzelm back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs; changeset | files
Sat, 13 Nov 2010 11:41:02 +0100 wenzelm await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion; changeset | files
Sat, 13 Nov 2010 00:24:41 +0100 wenzelm updated README; changeset | files
Fri, 12 Nov 2010 21:37:01 +0100 wenzelm defensive defaults for more robust experience for new users; changeset | files
Fri, 12 Nov 2010 17:44:03 +0100 wenzelm merged changeset | files
Fri, 12 Nov 2010 15:56:11 +0100 boehmes preliminary support for newer versions of Z3 changeset | files
Fri, 12 Nov 2010 15:56:10 +0100 boehmes turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user changeset | files
Fri, 12 Nov 2010 15:56:08 +0100 boehmes let the theory formally depend on the Boogie output changeset | files
Fri, 12 Nov 2010 15:56:07 +0100 boehmes look for certificates relative to the theory changeset | files
Fri, 12 Nov 2010 15:56:06 +0100 boehmes dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT changeset | files
Fri, 12 Nov 2010 06:11:29 -0800 huffman merged changeset | files
Fri, 12 Nov 2010 06:05:26 -0800 huffman update Theory.requires with new theory name changeset | files
Fri, 12 Nov 2010 14:51:28 +0100 wenzelm tuned signatures; changeset | files
Fri, 12 Nov 2010 14:06:37 +0100 wenzelm never open Unsynchronized; changeset | files
Fri, 12 Nov 2010 12:57:02 +0100 wenzelm merged changeset | files
Wed, 10 Nov 2010 18:45:48 -0800 huffman section headings changeset | files
Wed, 10 Nov 2010 18:37:11 -0800 huffman reorder chapters for generated document changeset | files
Wed, 10 Nov 2010 18:30:17 -0800 huffman merge Representable.thy into Domain.thy changeset | files
Wed, 10 Nov 2010 18:15:21 -0800 huffman move stuff from Domain.thy to Domain_Aux.thy changeset | files
Wed, 10 Nov 2010 17:56:08 -0800 huffman move map functions to new theory file Map_Functions; add theory file Plain_HOLCF changeset | files
Wed, 10 Nov 2010 14:59:52 -0800 huffman allow unpointed lazy arguments for definitional domain package changeset | files
Wed, 10 Nov 2010 14:20:47 -0800 huffman add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas changeset | files
Wed, 10 Nov 2010 13:22:39 -0800 huffman merged changeset | files
Wed, 10 Nov 2010 13:08:42 -0800 huffman removed unused lemma chain_mono2 changeset | files
Wed, 10 Nov 2010 11:42:35 -0800 huffman rename class 'bifinite' to 'domain' changeset | files
Wed, 10 Nov 2010 09:59:08 -0800 huffman instance sum :: (predomain, predomain) predomain changeset | files
Wed, 10 Nov 2010 09:52:50 -0800 huffman configure sum type for fixrec changeset | files
Wed, 10 Nov 2010 08:18:32 -0800 huffman add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a) changeset | files
Wed, 10 Nov 2010 06:02:37 -0800 huffman instance prod :: (predomain, predomain) predomain changeset | files
Tue, 09 Nov 2010 19:37:11 -0800 huffman adapt isodefl proof script to unpointed types changeset | files
Tue, 09 Nov 2010 16:37:13 -0800 huffman add 'predomain' class: unpointed version of bifinite changeset | files
Tue, 09 Nov 2010 08:41:36 -0800 huffman add bifiniteness check for domain_isomorphism command changeset | files
Tue, 09 Nov 2010 05:23:34 -0800 huffman implement map_of_typ using Pattern.rewrite_term changeset | files
Tue, 09 Nov 2010 04:47:46 -0800 huffman avoid using stale theory changeset | files
Mon, 08 Nov 2010 15:13:45 -0800 huffman implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data changeset | files
Mon, 08 Nov 2010 14:36:17 -0800 huffman add function the_sort changeset | files
Mon, 08 Nov 2010 14:09:07 -0800 huffman refactor tmp_thy code changeset | files
Mon, 08 Nov 2010 06:58:09 -0800 huffman reorganize Bifinite.thy; simplify some proofs related to bifinite class instances changeset | files
Fri, 12 Nov 2010 11:36:01 +0100 wenzelm treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space; changeset | files
Fri, 12 Nov 2010 10:58:09 +0100 wenzelm Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation; changeset | files
Thu, 11 Nov 2010 19:58:07 +0100 wenzelm more precise treatment of deleted nodes; changeset | files
Thu, 11 Nov 2010 18:55:17 +0100 wenzelm tuned error message; changeset | files
Thu, 11 Nov 2010 17:07:05 +0100 wenzelm unified type Document.Edit; changeset | files
Thu, 11 Nov 2010 16:48:46 +0100 wenzelm replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes; changeset | files
Thu, 11 Nov 2010 13:23:39 +0100 wenzelm tuned; changeset | files
Thu, 11 Nov 2010 13:07:41 +0100 wenzelm reduced danger of line breaks within minipage; changeset | files
Wed, 10 Nov 2010 20:43:22 +0100 wenzelm Sidekick block asset: show first line only; changeset | files
Wed, 10 Nov 2010 20:21:55 +0100 wenzelm added buffer_text convenience, with explicit locking; changeset | files
Wed, 10 Nov 2010 17:53:41 +0100 wenzelm use official/portable Multithreading.max_threads_value, which is also subject to user preferences (NB: Thread.numProcessors is apt to lead to surprises like very high numbers for systems with hyperthreading); changeset | files
Wed, 10 Nov 2010 16:05:15 +0100 wenzelm merged changeset | files
Wed, 10 Nov 2010 09:03:07 +0100 blanchet make SML/NJ happy changeset | files
Tue, 09 Nov 2010 16:18:40 +0100 haftmann merged changeset | files
Tue, 09 Nov 2010 14:02:14 +0100 haftmann slightly changed fun_map_def changeset | files
Tue, 09 Nov 2010 14:02:14 +0100 haftmann fun_rel_def is no simp rule by default changeset | files
Tue, 09 Nov 2010 14:02:13 +0100 haftmann more appropriate specification packages; fun_rel_def is no simp rule by default changeset | files
Tue, 09 Nov 2010 14:02:13 +0100 haftmann type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions changeset | files
Tue, 09 Nov 2010 14:02:13 +0100 haftmann more appropriate specification packages; fun_rel_def is no simp rule by default changeset | files
Tue, 09 Nov 2010 14:02:12 +0100 haftmann type annotations in specifications; fun_rel_def is no simp rule by default changeset | files
Tue, 09 Nov 2010 14:02:12 +0100 haftmann fun_rel_def is no simp rule by default changeset | files
Tue, 09 Nov 2010 14:00:10 +0000 paulson merged changeset | files
Tue, 09 Nov 2010 13:59:37 +0000 paulson tidied using metis changeset | files
Wed, 10 Nov 2010 15:59:23 +0100 wenzelm manage folding via sidekick by default; changeset | files
Wed, 10 Nov 2010 15:47:56 +0100 wenzelm eliminated obsolete heading category -- superseded by heading_level; changeset | files
Wed, 10 Nov 2010 15:43:06 +0100 wenzelm treat main theory commands like headings, and nest anything else inside; changeset | files
Wed, 10 Nov 2010 15:42:20 +0100 wenzelm proper treatment of equal heading level; changeset | files
Wed, 10 Nov 2010 15:41:29 +0100 wenzelm added missing Keyword.THY_SCHEMATIC_GOAL; changeset | files
Wed, 10 Nov 2010 15:17:25 +0100 wenzelm default Sidekick parser based on section headings; changeset | files
Wed, 10 Nov 2010 15:00:40 +0100 wenzelm some support for nested source structure, based on section headings; changeset | files
Wed, 10 Nov 2010 11:44:35 +0100 wenzelm tuned; changeset | files
Tue, 09 Nov 2010 23:24:46 +0100 wenzelm misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics); changeset | files
Tue, 09 Nov 2010 22:37:10 +0100 wenzelm updated version; changeset | files
Tue, 09 Nov 2010 21:52:05 +0100 wenzelm private counter, to keep externalized ids a bit smaller; changeset | files
Tue, 09 Nov 2010 21:44:19 +0100 wenzelm added general Synchronized.counter convenience; changeset | files
Tue, 09 Nov 2010 21:13:06 +0100 wenzelm explicitly identify forked/joined tasks; changeset | files
Tue, 09 Nov 2010 11:27:58 +0100 wenzelm accomodate old manuals that include pdfsetup.sty without isabelle.sty; changeset | files
Tue, 09 Nov 2010 11:17:15 +0100 wenzelm merged changeset | files
Mon, 08 Nov 2010 23:02:20 +0100 krauss removed type-inference-like behaviour from relation_tac completely; tuned changeset | files
Mon, 08 Nov 2010 20:55:27 +0100 wenzelm avoid clash of \<upharpoonright> vs. \<restriction> (cf. 666ea7e62384 and 3c49dbece0a8); changeset | files
Mon, 08 Nov 2010 20:50:56 +0100 wenzelm explicitly check uniqueness of symbol recoding; changeset | files
Mon, 08 Nov 2010 17:44:47 +0100 wenzelm more hints on building and running Isabelle/jEdit from command line; changeset | files
Mon, 08 Nov 2010 14:41:11 +0100 wenzelm merged changeset | files
Mon, 08 Nov 2010 14:33:54 +0100 blanchet merge changeset | files
Mon, 08 Nov 2010 14:33:30 +0100 blanchet reduce the number of monomorphization iterations from 10 (the default) to 4, in the interest of faster SMT solving changeset | files
Mon, 08 Nov 2010 05:07:18 -0800 huffman merged changeset | files
Sat, 06 Nov 2010 10:01:00 -0700 huffman merged changeset | files
Fri, 05 Nov 2010 15:15:28 -0700 huffman (infixl "<<" 55) -> (infix "<<" 50) changeset | files
Wed, 03 Nov 2010 17:22:25 -0700 huffman simplify some proofs changeset | files
Wed, 03 Nov 2010 17:06:21 -0700 huffman remove unnecessary stuff from Discrete.thy changeset | files
Wed, 03 Nov 2010 16:39:23 -0700 huffman remove some unnecessary lemmas; move monofun_LAM to Cfun.thy changeset | files
Wed, 03 Nov 2010 15:57:39 -0700 huffman add lemma eq_imp_below changeset | files
Wed, 03 Nov 2010 15:47:46 -0700 huffman discontinue a bunch of legacy theorem names changeset | files
Wed, 03 Nov 2010 15:31:24 -0700 huffman move a few admissibility lemmas into FOCUS/Stream_adm.thy changeset | files
Wed, 03 Nov 2010 15:03:16 -0700 huffman simplify some proofs changeset | files
Mon, 08 Nov 2010 13:53:18 +0100 blanchet compile -- 7550b2cba1cb broke the build changeset | files
Mon, 08 Nov 2010 13:25:00 +0100 blanchet merge changeset | files
Mon, 08 Nov 2010 09:10:44 +0100 blanchet recognize Vampire error changeset | files
Mon, 08 Nov 2010 12:13:51 +0100 boehmes return the process return code along with the process outputs changeset | files
Mon, 08 Nov 2010 12:13:44 +0100 boehmes better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures) changeset | files
Mon, 08 Nov 2010 11:49:28 +0100 haftmann merged changeset | files
Mon, 08 Nov 2010 10:56:48 +0100 haftmann corrected slip: must keep constant map, not type map; tuned code changeset | files
Mon, 08 Nov 2010 10:43:24 +0100 haftmann constructors to datatypes in code_reflect can be globbed; dropped unused code changeset | files
Mon, 08 Nov 2010 09:25:43 +0100 bulwahn adding code and theory for smallvalue generators, but do not setup the interpretation yet changeset | files
Mon, 08 Nov 2010 02:33:48 +0100 blanchet make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice changeset | files
Mon, 08 Nov 2010 02:32:27 +0100 blanchet better detection of completely irrelevant facts changeset | files
Sun, 07 Nov 2010 18:19:04 +0100 blanchet always use a hard timeout in Mirabelle changeset | files
Sun, 07 Nov 2010 18:15:13 +0100 blanchet use "smt" (rather than "metis") to reconstruct SMT proofs changeset | files
Sun, 07 Nov 2010 18:03:24 +0100 blanchet don't pass too many facts on the first iteration of the SMT solver changeset | files
Sun, 07 Nov 2010 18:02:02 +0100 blanchet catch TimeOut exception changeset | files
Sun, 07 Nov 2010 17:56:07 +0100 blanchet ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns changeset | files
Sun, 07 Nov 2010 17:51:25 +0100 blanchet if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed changeset | files
Sun, 07 Nov 2010 13:29:59 +0100 blanchet removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway changeset | files
Sat, 06 Nov 2010 10:25:08 +0100 blanchet make Nitpick datatype tests faster to make timeout less likely changeset | files
Sat, 06 Nov 2010 10:25:08 +0100 blanchet invoke SMT solver in a loop, with fewer and fewer facts, in case of error changeset | files
Sat, 06 Nov 2010 10:25:08 +0100 blanchet always honor the max relevant constraint changeset | files
Mon, 08 Nov 2010 11:28:22 +0100 wenzelm more robust treatment of suppressed quotes concerning replacement text -- for improved copy/paste behaviour; changeset | files
Mon, 08 Nov 2010 00:00:47 +0100 wenzelm updated generated files; changeset | files
Sun, 07 Nov 2010 23:32:26 +0100 wenzelm tweaked pdf setup to allow modification of \pdfminorversion; changeset | files
Sun, 07 Nov 2010 23:12:40 +0100 wenzelm merged; changeset | files
Sun, 07 Nov 2010 23:12:21 +0100 wenzelm updated generated files; changeset | files
Sun, 07 Nov 2010 22:51:16 +0100 wenzelm basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols; changeset | files
Sun, 07 Nov 2010 22:42:49 +0100 wenzelm updated generated file; changeset | files
Sun, 07 Nov 2010 22:26:25 +0100 wenzelm more literal appearance of antiqopen/antiqclose; changeset | files
Sun, 07 Nov 2010 16:39:03 +0100 wenzelm 'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises); changeset | files
Sat, 06 Nov 2010 20:59:59 +0100 wenzelm continue after failed commands; changeset | files
Sat, 06 Nov 2010 20:18:06 +0100 wenzelm added Keyword.is_heading (cf. Scala version); changeset | files
Sat, 06 Nov 2010 19:37:31 +0100 wenzelm updated keywords; changeset | files
Sat, 06 Nov 2010 19:36:54 +0100 wenzelm mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General; changeset | files
Sat, 06 Nov 2010 18:10:35 +0100 wenzelm somewhat more uniform timing markup in ML vs. Scala; changeset | files
Sat, 06 Nov 2010 17:55:32 +0100 wenzelm somewhat more uniform timing in ML vs. Scala; changeset | files
Sat, 06 Nov 2010 16:53:07 +0100 wenzelm added Markup.Double, Markup.Double_Property; changeset | files
Sat, 06 Nov 2010 16:31:35 +0100 wenzelm explicit "timing" status for toplevel transactions; changeset | files
Sat, 06 Nov 2010 16:03:49 +0100 wenzelm tuned; changeset | files
Sat, 06 Nov 2010 15:34:11 +0100 wenzelm tuned comments; changeset | files
Sat, 06 Nov 2010 00:10:32 +0100 krauss abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical changeset | files
Fri, 05 Nov 2010 23:19:20 +0100 wenzelm moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER; changeset | files
Fri, 05 Nov 2010 22:03:57 +0100 wenzelm updated keywords; changeset | files
Fri, 05 Nov 2010 22:01:01 +0100 wenzelm reflect actual content of /home/isabelle/.html-data/cgi-bin/hgwebdir.cgi; changeset | files
Fri, 05 Nov 2010 21:53:25 +0100 wenzelm eliminated spurious "firstline" filters for improved display of Isabelle history logs: one item per line, without special headline; changeset | files
Fri, 05 Nov 2010 21:48:48 +0100 wenzelm reflect actual content of /home/isabelle-repository/hgweb-templates/isabelle by krauss; changeset | files
Fri, 05 Nov 2010 21:42:32 +0100 wenzelm obsolete -- python installation on www4 is not modified (despite remaining "firstline" in graph and syndication views); changeset | files
Fri, 05 Nov 2010 19:47:20 +0100 wenzelm explicit indication of some remaining violations of the Isabelle/ML interrupt model; changeset | files
Fri, 05 Nov 2010 19:39:25 +0100 wenzelm updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already; changeset | files
Fri, 05 Nov 2010 19:22:04 +0100 wenzelm proper spelling; changeset | files
Fri, 05 Nov 2010 15:09:55 +0100 hoelzl merged changeset | files
Fri, 05 Nov 2010 14:17:18 +0100 hoelzl Extend convex analysis by Bogdan Grechuk changeset | files
Fri, 05 Nov 2010 14:36:17 +0100 blanchet merged changeset | files
Fri, 05 Nov 2010 09:49:03 +0100 blanchet fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2) changeset | files
Fri, 05 Nov 2010 09:05:22 +0100 blanchet make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information changeset | files
Thu, 04 Nov 2010 15:31:26 +0100 blanchet pass proper type to SMT_Builtin.is_builtin changeset | files
Thu, 04 Nov 2010 15:30:48 +0100 blanchet remove " s" suffix since seconds are now implicit changeset | files
Thu, 04 Nov 2010 14:59:44 +0100 blanchet ignore facts with only theory constants in them changeset | files
Thu, 04 Nov 2010 14:59:44 +0100 blanchet cosmetics changeset | files
Thu, 04 Nov 2010 14:59:44 +0100 blanchet use the SMT integration's official list of built-ins changeset | files
Fri, 05 Nov 2010 14:10:41 +0100 haftmann added class relation group_add < cancel_semigroup_add changeset | files
Fri, 05 Nov 2010 09:07:14 +0100 bulwahn merged changeset | files
Fri, 05 Nov 2010 08:16:35 +0100 bulwahn changing timeout to real value; handling Interrupt and Timeout more like nitpick does changeset | files
Fri, 05 Nov 2010 08:16:34 +0100 bulwahn added two lemmas about injectivity of concat to the list theory changeset | files
Fri, 05 Nov 2010 08:16:31 +0100 bulwahn adding documentation of some quickcheck options changeset | files
Fri, 05 Nov 2010 08:28:57 +0100 haftmann merged changeset | files
Thu, 04 Nov 2010 17:27:38 +0100 haftmann Code.check_const etc.: reject too specific types changeset | files
Thu, 04 Nov 2010 17:27:37 +0100 haftmann corrected quoting changeset | files
Thu, 04 Nov 2010 17:27:37 +0100 haftmann added lemma length_alloc changeset | files
Thu, 04 Nov 2010 13:42:36 +0100 haftmann dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document changeset | files
Thu, 04 Nov 2010 13:42:36 +0100 haftmann added note on countable types changeset | files
Thu, 04 Nov 2010 18:01:55 +0100 boehmes simulate more closely the behaviour of the tactic changeset | files
Thu, 04 Nov 2010 17:17:21 +0100 wenzelm merged changeset | files
Thu, 04 Nov 2010 13:37:11 +0100 haftmann merged changeset | files
Thu, 04 Nov 2010 09:54:16 +0100 haftmann merged changeset | files
Wed, 03 Nov 2010 14:14:06 +0100 haftmann dropped debug message changeset | files
Wed, 03 Nov 2010 14:14:06 +0100 haftmann more precise text changeset | files
Wed, 03 Nov 2010 14:14:05 +0100 haftmann SMLdummy target changeset | files
Wed, 03 Nov 2010 14:14:05 +0100 haftmann fixed typos changeset | files
Wed, 03 Nov 2010 12:20:33 +0100 haftmann moved theory Quicksort from Library/ to ex/ changeset | files
Wed, 03 Nov 2010 12:20:33 +0100 haftmann Theory Multiset provides stable quicksort implementation of sort_key. changeset | files
Wed, 03 Nov 2010 12:15:47 +0100 haftmann added code lemmas for stable parametrized quicksort changeset | files
Wed, 03 Nov 2010 11:50:29 +0100 haftmann tuned proof changeset | files
Thu, 04 Nov 2010 09:53:23 +0100 blanchet moved file in makefile to reflect actual dependencies changeset | files
Wed, 03 Nov 2010 23:01:30 +0100 blanchet give E one more second, to prevent cases where it finds a proof but has no time to print it changeset | files
Wed, 03 Nov 2010 22:51:32 +0100 blanchet use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages; changeset | files
Wed, 03 Nov 2010 22:33:23 +0100 blanchet don't be overly verbose in Sledgehammer's minimizer changeset | files
Wed, 03 Nov 2010 22:26:53 +0100 blanchet standardize on seconds for Nitpick and Sledgehammer timeouts changeset | files
Wed, 03 Nov 2010 20:19:24 +0100 nipkow cleaned up changeset | files
Thu, 04 Nov 2010 16:15:13 +0100 wenzelm added property "tooltip-margin"; changeset | files
Thu, 04 Nov 2010 10:58:03 +0100 wenzelm clarified tooltips: message output by default, extra info via control/command; changeset | files
Thu, 04 Nov 2010 10:33:37 +0100 wenzelm warn in correlation with report -- avoid spurious message duplicates; changeset | files
Thu, 04 Nov 2010 10:22:59 +0100 wenzelm tuned; changeset | files
Wed, 03 Nov 2010 21:53:56 +0100 wenzelm feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu); changeset | files
Wed, 03 Nov 2010 17:11:40 +0100 boehmes merged changeset | files
Wed, 03 Nov 2010 17:02:53 +0100 boehmes updated SMT certificates changeset | files
Wed, 03 Nov 2010 16:44:38 +0100 boehmes standardize timeout value based on reals changeset | files
Wed, 03 Nov 2010 15:56:15 +0100 wenzelm merged changeset | files
Wed, 03 Nov 2010 07:02:09 -0700 huffman merged changeset | files
Sat, 30 Oct 2010 15:13:11 -0700 huffman change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)' changeset | files
Sat, 30 Oct 2010 12:25:18 -0700 huffman merged changeset | files
Fri, 29 Oct 2010 17:15:28 -0700 huffman renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun changeset | files
Fri, 29 Oct 2010 16:51:40 -0700 huffman renamed lemma cont2cont_Rep_CFun to cont2cont_APP changeset | files
Fri, 29 Oct 2010 16:24:07 -0700 huffman simplify proof of typedef_cont_Abs changeset | files
Wed, 27 Oct 2010 15:50:01 -0700 huffman rename constant trifte to tr_case changeset | files
Wed, 27 Oct 2010 14:31:39 -0700 huffman add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t' changeset | files
Wed, 27 Oct 2010 14:15:54 -0700 huffman make syntax of continuous if-then-else consistent with HOL if-then-else changeset | files
Wed, 27 Oct 2010 13:54:18 -0700 huffman rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff changeset | files
Wed, 03 Nov 2010 10:44:53 +0100 haftmann polyml_as_definition does not require explicit dependencies on external ML files changeset | files
Wed, 03 Nov 2010 13:54:23 +0100 wenzelm explicit warning about opaque signature matching -- saves extra paragraph in implementation manual; changeset | files
Wed, 03 Nov 2010 11:33:51 +0100 wenzelm discontinued obsolete function sys_error and exception SYS_ERROR; changeset | files
Wed, 03 Nov 2010 11:11:49 +0100 wenzelm replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment; changeset | files
Wed, 03 Nov 2010 11:06:22 +0100 wenzelm replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment; changeset | files
Wed, 03 Nov 2010 10:51:40 +0100 wenzelm try_param_tac: plain user error appears more appropriate; changeset | files
Wed, 03 Nov 2010 10:48:55 +0100 wenzelm replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment; changeset | files
Wed, 03 Nov 2010 10:20:37 +0100 wenzelm eliminated dead code; changeset | files
Wed, 03 Nov 2010 10:18:05 +0100 wenzelm more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR; changeset | files
Wed, 03 Nov 2010 08:29:32 +0100 nipkow removed assumption changeset | files
Tue, 02 Nov 2010 21:59:21 +0100 wenzelm more on naming tactics; changeset | files
Tue, 02 Nov 2010 21:24:07 +0100 wenzelm merged changeset | files
Tue, 02 Nov 2010 20:32:33 +0100 haftmann merged changeset | files
Tue, 02 Nov 2010 16:59:40 +0100 haftmann tuned proof changeset | files
Tue, 02 Nov 2010 16:48:19 +0100 haftmann tuned proof changeset | files
Tue, 02 Nov 2010 16:36:33 +0100 haftmann tuned lemma proposition of properties_for_sort_key changeset | files
Tue, 02 Nov 2010 16:31:57 +0100 haftmann lemmas sorted_map_same, sorted_same changeset | files
Tue, 02 Nov 2010 16:31:56 +0100 haftmann lemmas multiset_of_filter, sort_key_by_quicksort changeset | files
Tue, 02 Nov 2010 21:21:07 +0100 wenzelm more on "Time" in Isabelle/ML; changeset | files
Tue, 02 Nov 2010 20:55:12 +0100 wenzelm simplified some time constants; changeset | files
Tue, 02 Nov 2010 20:31:46 +0100 wenzelm added convenience operation seconds: real -> time; changeset | files
Tue, 02 Nov 2010 20:16:56 +0100 wenzelm avoid catch-all exception handling; changeset | files
Tue, 02 Nov 2010 20:15:57 +0100 wenzelm eliminated fragile catch-all pattern, based on educated guess about the intended exception; changeset | files
Tue, 02 Nov 2010 12:37:12 +0100 traytel Attribute map_function -> coercion_map; changeset | files
Sun, 31 Oct 2010 13:26:37 +0100 wenzelm syntax category "real" subsumes plain "int"; changeset | files
Sun, 31 Oct 2010 11:45:45 +0100 nipkow merged changeset | files
Fri, 29 Oct 2010 17:57:36 +0200 nipkow Plus -> Sum_Type.Plus changeset | files
Sun, 31 Oct 2010 11:38:09 +0100 ballarin Minor reformat. changeset | files
Sat, 30 Oct 2010 21:08:20 +0200 wenzelm support for real valued preferences; changeset | files
Sat, 30 Oct 2010 16:33:58 +0200 wenzelm support for real valued configuration options; changeset | files
Sat, 30 Oct 2010 15:26:40 +0200 wenzelm support for floating-point tokens in outer syntax (coinciding with inner syntax version); changeset | files
Fri, 29 Oct 2010 23:15:01 +0200 wenzelm merged changeset | files
Fri, 29 Oct 2010 21:41:14 +0200 krauss added rule let_mono changeset | files
Fri, 29 Oct 2010 22:59:40 +0200 wenzelm CONTRIBUTORS; changeset | files
Fri, 29 Oct 2010 22:54:54 +0200 wenzelm more sharing of operations, without aliases; changeset | files
Fri, 29 Oct 2010 22:22:36 +0200 wenzelm simplified data lookup; changeset | files
Fri, 29 Oct 2010 22:19:27 +0200 wenzelm export declarations by default, to allow other ML packages by-pass concrete syntax; changeset | files
Fri, 29 Oct 2010 22:07:48 +0200 wenzelm proper signature constraint for ML structure; changeset | files
Fri, 29 Oct 2010 21:49:33 +0200 wenzelm proper header; changeset | files
Fri, 29 Oct 2010 21:34:07 +0200 wenzelm Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010). changeset | files
Fri, 29 Oct 2010 18:17:11 +0200 boehmes updated SMT certificates changeset | files
Fri, 29 Oct 2010 18:17:10 +0200 boehmes eta-expand built-in constants; also rewrite partially applied natural number terms changeset | files
Fri, 29 Oct 2010 18:17:09 +0200 boehmes optionally drop assumptions which cannot be preprocessed changeset | files
Fri, 29 Oct 2010 18:17:08 +0200 boehmes added crafted list of SMT built-in constants changeset | files
Fri, 29 Oct 2010 18:17:06 +0200 boehmes clarified error message changeset | files
Fri, 29 Oct 2010 18:17:05 +0200 boehmes tuned changeset | files
Fri, 29 Oct 2010 18:17:04 +0200 boehmes introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list changeset | files
Fri, 29 Oct 2010 17:38:57 +0200 wenzelm merged changeset | files
Fri, 29 Oct 2010 17:28:27 +0200 nipkow added listrel1 changeset | files
Fri, 29 Oct 2010 17:25:22 +0200 nipkow hide Sum_Type.Plus changeset | files
Fri, 29 Oct 2010 16:51:20 +0200 wenzelm merged changeset | files
Fri, 29 Oct 2010 16:04:35 +0200 haftmann added user aliasses (still unclear how to specify names with whitespace contained) changeset | files
Fri, 29 Oct 2010 14:06:10 +0200 haftmann merged changeset | files
Fri, 29 Oct 2010 14:03:02 +0200 haftmann tuned structure of theory changeset | files
Fri, 29 Oct 2010 13:49:49 +0200 haftmann remove term_of equations for Heap type explicitly changeset | files
Fri, 29 Oct 2010 12:49:05 +0200 blanchet no need for setting up the kodkodi environment since Kodkodi 1.2.9 changeset | files
Fri, 29 Oct 2010 12:49:05 +0200 blanchet fixed order of quantifier instantiation in new Skolemizer changeset | files
Fri, 29 Oct 2010 12:49:05 +0200 blanchet restructure Skolemization code slightly changeset | files
Fri, 29 Oct 2010 12:49:05 +0200 blanchet ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer) changeset | files
Fri, 29 Oct 2010 12:49:05 +0200 blanchet more work on new Skolemizer without Hilbert_Choice changeset | files
Fri, 29 Oct 2010 12:49:05 +0200 blanchet fix cluster numbering in the absense of Hilbert_Choice (reverts acde1b606b0e, effectively reintroducing most of 0bfaaa81fc62) changeset | files
Fri, 29 Oct 2010 12:49:05 +0200 blanchet prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems changeset | files
Fri, 29 Oct 2010 12:49:05 +0200 blanchet make handling of parameters more robust, by querying the goal changeset | files
Fri, 29 Oct 2010 11:35:28 +0200 haftmann actually pass "verbose" argument changeset | files
Fri, 29 Oct 2010 16:16:10 +0200 wenzelm eliminated obsolete \_ escape; changeset | files
Fri, 29 Oct 2010 11:49:56 +0200 wenzelm eliminated obsolete \_ escapes in rail environments; changeset | files
Fri, 29 Oct 2010 11:35:47 +0200 wenzelm proper markup of formal text; changeset | files
Fri, 29 Oct 2010 11:07:21 +0200 wenzelm merged changeset | files
Fri, 29 Oct 2010 11:04:41 +0200 krauss hide_const various constants, in particular to avoid ugly qualifiers in HOLCF changeset | files
Fri, 29 Oct 2010 10:40:36 +0200 blanchet reverted e31e3f0071d4 because "foo.bar(5)" (with quotes) is wrong changeset | files
Fri, 29 Oct 2010 10:14:49 +0200 Lars Noschinski merged changeset | files
Wed, 22 Sep 2010 09:56:39 +0200 Lars Noschinski Remove unnecessary premise of mult1_union changeset | files
Fri, 29 Oct 2010 08:44:49 +0200 bulwahn adapting HOL-Mutabelle to changes in quickcheck changeset | files
Fri, 29 Oct 2010 08:44:46 +0200 bulwahn NEWS changeset | files
Fri, 29 Oct 2010 08:44:44 +0200 bulwahn changed global fixed timeout to a configurable timeout for quickcheck; test parameters in quickcheck are now fully passed around with the context changeset | files
Fri, 29 Oct 2010 08:44:43 +0200 bulwahn updating documentation on quickcheck in the Isar reference changeset | files
Thu, 28 Oct 2010 18:36:34 +0200 bulwahn merged changeset | files
Thu, 28 Oct 2010 17:28:45 +0200 bulwahn adding a simple check to only run with a SWI-Prolog version known to work changeset | files
Thu, 28 Oct 2010 23:54:39 +0200 wenzelm tuned messages; changeset | files
Thu, 28 Oct 2010 23:19:52 +0200 wenzelm discontinued obsolete ML antiquotation @{theory_ref}; changeset | files
Thu, 28 Oct 2010 22:59:33 +0200 wenzelm tuned; changeset | files
Thu, 28 Oct 2010 22:39:59 +0200 wenzelm moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref; changeset | files
Thu, 28 Oct 2010 22:23:11 +0200 wenzelm type attribute is derived concept outside the kernel; changeset | files
Thu, 28 Oct 2010 22:12:08 +0200 wenzelm preserve original source position of exn; changeset | files
Thu, 28 Oct 2010 22:11:06 +0200 wenzelm handle Type.TYPE_MATCH, not arbitrary exceptions via MATCH_TYPE variable; changeset | files
Thu, 28 Oct 2010 22:04:00 +0200 wenzelm use Exn.interruptible_capture to keep user-code interruptible (Exn.capture not immediately followed by Exn.release here); changeset | files
Thu, 28 Oct 2010 21:59:01 +0200 wenzelm added Exn.interruptible_capture, which reraises interrupts as required by user-code (when Exn.capture is not immediately followed by Exn.release); changeset | files
Thu, 28 Oct 2010 21:52:33 +0200 wenzelm eliminated dead code; changeset | files
Thu, 28 Oct 2010 21:51:34 +0200 wenzelm tuned white-space; changeset | files
Thu, 28 Oct 2010 17:54:25 +0200 nipkow merged changeset | files
Thu, 28 Oct 2010 17:54:09 +0200 nipkow added lemmas about listrel(1) changeset | files
Thu, 28 Oct 2010 17:25:46 +0200 wenzelm tuned; changeset | files
Thu, 28 Oct 2010 15:10:34 +0200 wenzelm merged changeset | files
Thu, 28 Oct 2010 12:33:24 +0200 blanchet support non-identifier-like fact names in Sledgehammer (e.g., "my lemma") by quoting them changeset | files
Thu, 28 Oct 2010 10:38:29 +0200 blanchet merged changeset | files
Thu, 28 Oct 2010 09:40:57 +0200 blanchet clear identification changeset | files
Thu, 28 Oct 2010 09:36:51 +0200 blanchet clear identification; changeset | files
Thu, 28 Oct 2010 09:29:57 +0200 blanchet clear identification changeset | files
Wed, 27 Oct 2010 19:14:33 +0200 blanchet reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try) changeset | files
Wed, 27 Oct 2010 16:32:13 +0200 blanchet do not let Metis be confused by higher-order reasoning leading to literals of the form "~ ~ p", which are really the same as "p" changeset | files
Wed, 27 Oct 2010 09:22:40 +0200 blanchet generalize to handle any prover (not just E) changeset | files
Wed, 27 Oct 2010 11:11:35 -0700 huffman merged changeset | files
Wed, 27 Oct 2010 11:10:36 -0700 huffman make domain package work with non-cpo argument types changeset | files
Wed, 27 Oct 2010 11:06:53 -0700 huffman make op -->> infixr, to match op ---> changeset | files
Tue, 26 Oct 2010 14:19:59 -0700 huffman use Named_Thms instead of Theory_Data for some domain package theorems changeset | files
Tue, 26 Oct 2010 09:00:07 -0700 huffman change types of ML commands add_domain, add_new_domain to take 'sort' instead of 'string option' changeset | files
Tue, 26 Oct 2010 08:36:52 -0700 huffman use Term.add_tfreesT changeset | files
Sun, 24 Oct 2010 15:42:57 -0700 huffman rename case combinators generated by domain package to 'foo_case' instead of 'foo_when' changeset | files
Sun, 24 Oct 2010 15:19:17 -0700 huffman rename constant 'one_when' to 'one_case' changeset | files
Wed, 27 Oct 2010 16:40:34 +0200 haftmann merged changeset | files
Wed, 27 Oct 2010 16:40:31 +0200 haftmann sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas changeset | files
Wed, 27 Oct 2010 13:46:30 +0200 krauss regenerated keyword file changeset | files
Wed, 27 Oct 2010 08:58:03 +0200 boehmes made SML/NJ happy changeset | files
Tue, 26 Oct 2010 21:51:04 +0200 blanchet adapted SMT solver error handling to reflect latest changes in "SMT_Solver" changeset | files
Tue, 26 Oct 2010 21:43:50 +0200 blanchet better list of irrelevant SMT constants changeset | files
Tue, 26 Oct 2010 21:34:01 +0200 blanchet if "debug" is on, print list of relevant facts (poweruser request); changeset | files
Tue, 26 Oct 2010 21:01:28 +0200 blanchet standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module changeset | files
Tue, 26 Oct 2010 20:12:33 +0200 blanchet "Nitpick" -> "Sledgehammer"; changeset | files
Tue, 26 Oct 2010 20:09:38 +0200 blanchet merge changeset | files
Tue, 26 Oct 2010 16:59:19 +0200 blanchet merged changeset | files
Tue, 26 Oct 2010 16:56:54 +0200 blanchet remove needless context argument; changeset | files
Tue, 26 Oct 2010 17:35:54 +0200 boehmes use proper context changeset | files
Tue, 26 Oct 2010 17:35:52 +0200 boehmes trace assumptions before giving them to the SMT solver changeset | files
Tue, 26 Oct 2010 17:35:51 +0200 boehmes capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1 changeset | files
Tue, 26 Oct 2010 17:35:49 +0200 boehmes honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter changeset | files
Tue, 26 Oct 2010 16:39:21 +0200 haftmann include ATP in theory List -- avoid theory edge by-passing the prominent list theory changeset | files
Tue, 26 Oct 2010 15:06:36 +0200 krauss fixed typo changeset | files
Tue, 26 Oct 2010 15:01:39 +0200 blanchet merged changeset | files
Tue, 26 Oct 2010 15:01:02 +0200 blanchet merged changeset | files
Tue, 26 Oct 2010 14:49:48 +0200 blanchet put theorems added using "add:" at the beginning of the list returned by the relevance filter, so that they don't get truncated away changeset | files
Tue, 26 Oct 2010 14:48:55 +0200 blanchet tuning changeset | files
Tue, 26 Oct 2010 15:00:57 +0200 haftmann merged changeset | files
Tue, 26 Oct 2010 14:06:22 +0200 haftmann consider base sorts of superclasses simultaneously during processing of class specification -- avoids clash of different base sorts changeset | files
Tue, 26 Oct 2010 15:00:42 +0200 haftmann more general treatment of type argument in code certificates for operations on abstract types changeset | files
Tue, 26 Oct 2010 14:11:34 +0200 haftmann partial_function is a declaration command changeset | files
Tue, 26 Oct 2010 14:06:21 +0200 blanchet merged changeset | files
Tue, 26 Oct 2010 13:50:57 +0200 blanchet proper error handling for SMT solvers in Sledgehammer changeset | files
Tue, 26 Oct 2010 13:50:18 +0200 krauss NEWS changeset | files
Tue, 26 Oct 2010 13:17:37 +0200 blanchet merge changeset | files
Tue, 26 Oct 2010 13:16:43 +0200 blanchet integrated "smt" proof method with Sledgehammer changeset | files
Tue, 26 Oct 2010 13:19:31 +0200 krauss fixed confusion introduced in 008dc2d2c395 changeset | files
Tue, 26 Oct 2010 12:23:39 +0200 blanchet merged changeset | files
Tue, 26 Oct 2010 12:17:19 +0200 blanchet reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers changeset | files
Tue, 26 Oct 2010 12:19:31 +0200 haftmann merged changeset | files
Tue, 26 Oct 2010 12:19:22 +0200 haftmann tuned changeset | files
Tue, 26 Oct 2010 12:21:45 +0200 krauss merged changeset | files
Tue, 26 Oct 2010 12:19:02 +0200 krauss use partial_function instead of MREC combinator; curried rev' changeset | files
Tue, 26 Oct 2010 12:19:02 +0200 krauss added Heap monad instance of partial_function package changeset | files
Tue, 26 Oct 2010 12:19:02 +0200 krauss added Spec_Rule declaration to partial_function changeset | files
Tue, 26 Oct 2010 12:19:01 +0200 krauss basic documentation for command partial_function changeset | files
Tue, 26 Oct 2010 12:19:01 +0200 krauss remove outdated "(otherwise)" syntax from manual changeset | files
Tue, 26 Oct 2010 12:19:01 +0200 krauss declare recursive equation as ".simps", in accordance with other packages changeset | files
Tue, 26 Oct 2010 12:16:08 +0200 haftmann merged changeset | files
Tue, 26 Oct 2010 12:15:55 +0200 haftmann dropped accidental doubled computation changeset | files
Tue, 26 Oct 2010 11:51:09 +0200 boehmes optionally force the remote version of an SMT solver to be executed changeset | files
Tue, 26 Oct 2010 11:49:36 +0200 boehmes tuned changeset | files
Tue, 26 Oct 2010 11:49:23 +0200 boehmes added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed) changeset | files
Tue, 26 Oct 2010 11:46:19 +0200 boehmes changed SMT configuration options; updated SMT certificates changeset | files
Tue, 26 Oct 2010 11:45:12 +0200 boehmes joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface changeset | files
Tue, 26 Oct 2010 11:39:26 +0200 boehmes keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs changeset | files
Tue, 26 Oct 2010 11:31:03 +0200 blanchet merged changeset | files
Tue, 26 Oct 2010 11:21:08 +0200 blanchet merge changeset | files
Tue, 26 Oct 2010 11:11:23 +0200 blanchet clearer error messages changeset | files
Tue, 26 Oct 2010 11:10:00 +0200 blanchet renaming changeset | files
Thu, 28 Oct 2010 15:06:47 +0200 wenzelm back again to non-Apple font rendering (cf. 4977324373f2); changeset | files
Thu, 28 Oct 2010 14:56:14 +0200 wenzelm dock isabelle-session at bottom (again, cf. 37bdc2220cf8) to ensure that controls are fully visible; changeset | files
Tue, 26 Oct 2010 16:56:07 +0200 wenzelm disable broken popups for now; changeset | files
Tue, 26 Oct 2010 15:57:16 +0200 wenzelm tuned; changeset | files
Tue, 26 Oct 2010 11:31:22 +0200 wenzelm do not handle arbitrary exceptions; changeset | files
Tue, 26 Oct 2010 11:23:27 +0200 wenzelm merged changeset | files
Tue, 26 Oct 2010 11:20:14 +0200 haftmann Code_Runtime.trace changeset | files
Tue, 26 Oct 2010 11:22:18 +0200 wenzelm proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim}; changeset | files
Tue, 26 Oct 2010 11:06:12 +0200 wenzelm merged changeset | files
Tue, 26 Oct 2010 11:00:17 +0200 blanchet improved English changeset | files
Tue, 26 Oct 2010 10:59:28 +0200 blanchet whitespace tuning changeset | files
Tue, 26 Oct 2010 10:57:04 +0200 blanchet no need to encode theorem number twice in skolem names changeset | files
Tue, 26 Oct 2010 10:39:52 +0200 blanchet tuning changeset | files
Tue, 26 Oct 2010 09:40:20 +0200 blanchet make SML/NJ happy changeset | files
Mon, 25 Oct 2010 21:17:16 +0200 bulwahn relaxing the filtering condition for getting specifications from Spec_Rules changeset | files
Mon, 25 Oct 2010 21:17:16 +0200 bulwahn adding new predicate compiler files to the IsaMakefile changeset | files
Mon, 25 Oct 2010 21:17:15 +0200 bulwahn using mode_eq instead of op = for lookup in the predicate compiler changeset | files
Mon, 25 Oct 2010 21:17:14 +0200 bulwahn renaming split_modeT' to split_modeT changeset | files
Mon, 25 Oct 2010 21:17:13 +0200 bulwahn options as first argument to check functions changeset | files
Mon, 25 Oct 2010 21:17:12 +0200 bulwahn changing test parameters in examples to get to a result within the global timelimit changeset | files
Mon, 25 Oct 2010 21:17:11 +0200 bulwahn adding a global fixed timeout to quickcheck changeset | files
Mon, 25 Oct 2010 21:17:10 +0200 bulwahn adding a global time limit to the values command changeset | files
Mon, 25 Oct 2010 22:47:02 +0200 wenzelm explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt; changeset | files
Mon, 25 Oct 2010 21:23:09 +0200 wenzelm more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now); changeset | files
Mon, 25 Oct 2010 21:06:56 +0200 wenzelm renamed Output.priority to Output.urgent_message to emphasize its special role more clearly; changeset | files
Mon, 25 Oct 2010 20:24:13 +0200 wenzelm explicitly qualify type Output.output, which is a slightly odd internal feature; changeset | files
Mon, 25 Oct 2010 16:52:20 +0200 wenzelm export main ML entry by default; changeset | files
Mon, 25 Oct 2010 16:41:23 +0200 wenzelm observe Isabelle/ML coding standards; changeset | files
Mon, 25 Oct 2010 16:18:00 +0200 wenzelm merged changeset | files
Mon, 25 Oct 2010 16:17:16 +0200 wenzelm significantly improved Isabelle/Isar implementation manual; changeset | files
Mon, 25 Oct 2010 16:14:40 +0200 wenzelm misc tuning; changeset | files
Mon, 25 Oct 2010 11:39:52 +0200 wenzelm removed some remains of Output.debug (follow-up to fce2202892c4); changeset | files
Mon, 25 Oct 2010 11:22:30 +0200 wenzelm recovered some odd two-dimensional layout; changeset | files
Mon, 25 Oct 2010 13:36:20 +0200 haftmann merged changeset | files
Mon, 25 Oct 2010 13:34:58 +0200 haftmann dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps changeset | files
Mon, 25 Oct 2010 13:34:57 +0200 haftmann moved sledgehammer to Plain; tuned dependencies changeset | files
Mon, 25 Oct 2010 13:34:57 +0200 haftmann CONTRIBUTORS changeset | files
Mon, 25 Oct 2010 12:24:38 +0200 blanchet merge changeset | files
Mon, 25 Oct 2010 11:42:05 +0200 blanchet merged changeset | files
Mon, 25 Oct 2010 10:38:41 +0200 blanchet updated keywords changeset | files
Mon, 25 Oct 2010 10:30:46 +0200 blanchet introduced manual version of "Auto Solve" as "solve_direct" changeset | files
Mon, 25 Oct 2010 09:29:43 +0200 blanchet make "sledgehammer_params" work on single-threaded platforms changeset | files
Fri, 22 Oct 2010 18:31:45 +0200 blanchet tuning changeset | files
Fri, 22 Oct 2010 18:24:10 +0200 blanchet handle timeouts (to prevent failure from other threads); changeset | files
Mon, 25 Oct 2010 12:11:12 +0200 haftmann update keywords changeset | files
Mon, 25 Oct 2010 10:45:22 +0200 krauss some partial_function examples changeset | files
Mon, 25 Oct 2010 11:16:23 +0200 wenzelm added ML antiquotation @{assert}; changeset | files
Mon, 25 Oct 2010 11:01:00 +0200 wenzelm updated keywords; changeset | files
Sat, 23 Oct 2010 23:42:04 +0200 krauss integrated partial_function into HOL-Plain changeset | files
Sat, 23 Oct 2010 23:41:19 +0200 krauss first version of partial_function package changeset | files
Sat, 23 Oct 2010 23:39:37 +0200 krauss Complete_Partial_Order.thy: complete partial orders over arbitrary chains, with fixpoint theorem changeset | files
Mon, 25 Oct 2010 08:08:08 +0200 bulwahn merged changeset | files
Fri, 22 Oct 2010 18:38:59 +0200 bulwahn splitting Hotel Key card example into specification and the two tests for counter example generation changeset | files
Fri, 22 Oct 2010 18:38:59 +0200 bulwahn adding generator quickcheck changeset | files
Fri, 22 Oct 2010 18:38:59 +0200 bulwahn restructuring values command and adding generator compilation changeset | files
Fri, 22 Oct 2010 18:38:59 +0200 bulwahn moving general functions from core_data to predicate_compile_aux changeset | files
Fri, 22 Oct 2010 18:38:59 +0200 bulwahn updating to new notation in commented examples changeset | files
Sun, 24 Oct 2010 15:11:24 -0700 huffman merged changeset | files
Sun, 24 Oct 2010 03:43:12 -0700 huffman use default names sprod/Rep_sprod/Abs_sprod from pcpodef instead of Sprod/Rep_Sprod/Abs_Sprod; similarly for ssum changeset | files
Sat, 23 Oct 2010 19:56:33 -0700 huffman remove legacy comp_dbind option from domain package changeset | files
Sat, 23 Oct 2010 11:04:26 -0700 huffman change fixrec parser to not accept theorem names with (unchecked) option changeset | files
Sat, 23 Oct 2010 11:03:50 -0700 huffman tuned changeset | files
Fri, 22 Oct 2010 15:49:18 -0700 huffman rename lemma surjective_pairing_Sprod2 to spair_sfst_ssnd changeset | files
Fri, 22 Oct 2010 15:47:43 -0700 huffman add lemma strict3 changeset | files
Fri, 22 Oct 2010 11:24:52 -0700 huffman do proofs using Rep_Sprod_simps, Rep_Ssum_simps; remove unused lemmas changeset | files
Fri, 22 Oct 2010 07:45:32 -0700 huffman make discrete_cpo a subclass of chfin; remove chfin instances for fun, cfun changeset | files
Fri, 22 Oct 2010 07:44:34 -0700 huffman direct instantiation unit :: discrete_cpo changeset | files
Fri, 22 Oct 2010 06:58:45 -0700 huffman remove finite_po class changeset | files
Fri, 22 Oct 2010 06:08:51 -0700 huffman simplify proofs about flift; remove unneeded lemmas changeset | files
Fri, 22 Oct 2010 05:54:54 -0700 huffman simplify proof changeset | files
Thu, 21 Oct 2010 15:21:39 -0700 huffman minimize imports changeset | files
Thu, 21 Oct 2010 15:19:07 -0700 huffman add type annotation to avoid warning changeset | files
Thu, 21 Oct 2010 12:51:36 -0700 huffman simplify some proofs, convert to Isar style changeset | files
Thu, 21 Oct 2010 12:03:49 -0700 huffman rename lemma spair_lemma to spair_Sprod changeset | files
Thu, 21 Oct 2010 06:03:18 -0700 huffman pcpodef (open) 'a lift changeset | files
Thu, 21 Oct 2010 05:44:38 -0700 huffman remove intro! attribute from {sinl,sinr}_defined changeset | files
Thu, 21 Oct 2010 05:35:32 -0700 huffman simplify proofs of ssumE, sprodE changeset | files
Sun, 24 Oct 2010 21:25:13 +0200 wenzelm merged changeset | files
Sun, 24 Oct 2010 20:37:30 +0200 nipkow renamed nat_number changeset | files
Sun, 24 Oct 2010 20:19:00 +0200 nipkow nat_number -> eval_nat_numeral changeset | files
Fri, 22 Oct 2010 23:45:20 +0200 krauss some cleanup in Function_Lib changeset | files
Fri, 22 Oct 2010 17:15:46 +0200 blanchet merged changeset | files
Fri, 22 Oct 2010 16:45:55 +0200 blanchet compile changeset | files
Fri, 22 Oct 2010 16:37:11 +0200 blanchet added SMT solver to Sledgehammer docs changeset | files
Fri, 22 Oct 2010 16:11:43 +0200 blanchet more robust handling of "remote_" vs. non-"remote_" provers changeset | files
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) changeset | files
Fri, 22 Oct 2010 14:47:43 +0200 blanchet replaced references with proper record that's threaded through changeset | files
Fri, 22 Oct 2010 14:10:32 +0200 blanchet fixed signature of "is_smt_solver_installed"; changeset | files
Fri, 22 Oct 2010 13:57:54 +0200 blanchet renamed modules changeset | files
Fri, 22 Oct 2010 13:54:51 +0200 blanchet renamed files changeset | files
Fri, 22 Oct 2010 13:49:44 +0200 blanchet took out "smt"/"remote_smt" from default ATPs until they are properly implemented changeset | files
Fri, 22 Oct 2010 13:48:21 +0200 blanchet remove more needless code ("run_smt_solvers"); changeset | files
Fri, 22 Oct 2010 12:15:31 +0200 blanchet got rid of duplicate functionality ("run_smt_solver_somehow"); changeset | files
Fri, 22 Oct 2010 11:58:33 +0200 blanchet bring ATPs and SMT solvers more in line with each other changeset | files
Fri, 22 Oct 2010 11:11:34 +0200 blanchet make Sledgehammer minimizer fully work with SMT changeset | files
Fri, 22 Oct 2010 09:50:18 +0200 blanchet generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well changeset | files
Thu, 21 Oct 2010 16:25:40 +0200 blanchet first step in adding support for an SMT backend to Sledgehammer changeset | files
Thu, 21 Oct 2010 14:55:09 +0200 blanchet use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..." changeset | files
Thu, 21 Oct 2010 14:54:39 +0200 blanchet cosmetics changeset | files
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 changeset | files
Fri, 22 Oct 2010 12:01:12 +0200 hoelzl Changed section title to please LaTeX. changeset | files
Thu, 21 Oct 2010 20:26:35 +0200 bulwahn temporary removed Predicate_Compile_Quickcheck_Examples from tests changeset | files
Thu, 21 Oct 2010 19:13:11 +0200 bulwahn adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog changeset | files
Thu, 21 Oct 2010 19:13:10 +0200 bulwahn using a signature in core_data and moving some more functions to core_data changeset | files
Thu, 21 Oct 2010 19:13:09 +0200 bulwahn splitting large core file into core_data, mode_inference and predicate_compile_proof changeset | files
Thu, 21 Oct 2010 19:13:09 +0200 bulwahn added generator_dseq compilation for a sound depth-limited compilation with small value generators changeset | files
Thu, 21 Oct 2010 19:13:08 +0200 bulwahn for now safely but unpractically assume no predicate is terminating changeset | files
Thu, 21 Oct 2010 19:13:07 +0200 bulwahn adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible changeset | files
Thu, 21 Oct 2010 19:13:06 +0200 bulwahn adding option smart_depth_limiting to predicate compiler changeset | files
Wed, 20 Oct 2010 21:26:51 -0700 huffman merged changeset | files
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 changeset | files
Wed, 20 Oct 2010 17:25:22 -0700 huffman add lemma lub_eq_bottom_iff changeset | files
Wed, 20 Oct 2010 16:19:25 -0700 huffman combine check_and_sort_domain with main function; rewrite much of the error-checking code changeset | files
Wed, 20 Oct 2010 13:22:30 -0700 huffman constructor arguments with selectors must have pointed types changeset | files
Wed, 20 Oct 2010 13:02:13 -0700 huffman simplify check_and_sort_domain; more meaningful variable names changeset | files
Tue, 19 Oct 2010 16:21:24 -0700 huffman replace fixrec 'permissive' mode with per-equation 'unchecked' option changeset | files
Tue, 19 Oct 2010 15:01:51 -0700 huffman rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML changeset | files
Tue, 19 Oct 2010 14:28:14 -0700 huffman simplify some proofs; remove some unused lists of lemmas changeset | files
Tue, 19 Oct 2010 11:07:42 -0700 huffman replace 'in_defl' relation and '_ ::: _' syntax with 'defl_set' function changeset | files
Tue, 19 Oct 2010 10:13:29 -0700 huffman eliminate constant 'coerce'; use 'prj oo emb' instead changeset | files
Tue, 19 Oct 2010 07:05:04 -0700 huffman simplify fixrec pattern match function changeset | files
Sun, 17 Oct 2010 09:53:47 -0700 huffman simplify some proofs changeset | files
Tue, 19 Oct 2010 15:13:35 +0100 Christian Urban tuned changeset | files
Tue, 19 Oct 2010 12:26:38 +0200 bulwahn added some facts about factorial and dvd, div and mod changeset | files
Tue, 19 Oct 2010 12:26:37 +0200 bulwahn removing something that probably slipped into the Quotient_List theory changeset | files
Tue, 19 Oct 2010 11:44:42 +0900 Cezary Kaliszyk Quotient package: partial equivalence introduction changeset | files
Mon, 18 Oct 2010 14:25:15 +0100 Christian Urban reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset) changeset | files
Sat, 16 Oct 2010 17:10:23 -0700 huffman remove dead code changeset | files
Sat, 16 Oct 2010 17:09:57 -0700 huffman remove old uses of 'simp_tac HOLCF_ss' changeset | files
Sat, 16 Oct 2010 16:39:06 -0700 huffman merged changeset | files
Sat, 16 Oct 2010 16:22:42 -0700 huffman remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check changeset | files
Sat, 16 Oct 2010 15:26:30 -0700 huffman reimplement proof automation for coinduct rules changeset | files
Sat, 16 Oct 2010 14:41:11 -0700 huffman add functions mk_imp, mk_all changeset | files
Fri, 15 Oct 2010 08:52:53 -0700 huffman move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code changeset | files
Fri, 15 Oct 2010 08:07:20 -0700 huffman simplify automation of induct proof changeset | files
Fri, 15 Oct 2010 06:08:42 -0700 huffman add function mk_adm changeset | files
Fri, 15 Oct 2010 05:50:27 -0700 huffman rewrite proof automation for finite_ind; get rid of case_UU_tac changeset | files
Thu, 14 Oct 2010 19:16:52 -0700 huffman put constructor argument specs in constr_info type changeset | files
Thu, 14 Oct 2010 14:42:05 -0700 huffman avoid using Global_Theory.get_thm changeset | files
Thu, 14 Oct 2010 13:46:27 -0700 huffman include iso_info as part of constr_info type changeset | files
Thu, 14 Oct 2010 13:28:31 -0700 huffman remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors changeset | files
Thu, 14 Oct 2010 10:16:46 -0700 huffman add take_strict_thms field to take_info type changeset | files
Thu, 14 Oct 2010 09:44:40 -0700 huffman add record type synonym 'constr_info' changeset | files
Thu, 14 Oct 2010 09:34:00 -0700 huffman add function take_theorems changeset | files
Thu, 14 Oct 2010 09:28:05 -0700 huffman add type annotation to avoid warning changeset | files
Wed, 13 Oct 2010 10:56:42 -0700 huffman cleaned up Fun_Cpo.thy; deprecated a few theorem names changeset | files
Wed, 13 Oct 2010 10:27:26 -0700 huffman edit comments changeset | files
Tue, 12 Oct 2010 09:32:21 -0700 huffman remove unneeded lemmas Lift_exhaust, Lift_cases changeset | files
Tue, 12 Oct 2010 09:08:27 -0700 huffman move lemmas from Lift.thy to Cfun.thy changeset | files
Tue, 12 Oct 2010 07:46:44 -0700 huffman cleaned up Adm.thy changeset | files
Tue, 12 Oct 2010 06:20:05 -0700 huffman remove unneeded lemmas from Fun_Cpo.thy changeset | files
Tue, 12 Oct 2010 05:48:32 -0700 huffman remove unused lemmas changeset | files
Tue, 12 Oct 2010 05:48:15 -0700 huffman reformulate lemma cont2cont_lub and move to Cont.thy changeset | files
Tue, 12 Oct 2010 05:25:21 -0700 huffman remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2 changeset | files
Mon, 11 Oct 2010 21:35:31 -0700 huffman new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI changeset | files
Mon, 11 Oct 2010 16:24:44 -0700 huffman rename Ffun.thy to Fun_Cpo.thy changeset | files
Mon, 11 Oct 2010 16:14:15 -0700 huffman remove unused constant 'directed' changeset | files
Mon, 11 Oct 2010 09:54:04 -0700 huffman add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite changeset | files
Fri, 15 Oct 2010 17:21:37 +0100 paulson merged changeset | files
Fri, 15 Oct 2010 17:21:07 +0100 paulson prevention of self-referential type environments changeset | files
Fri, 15 Oct 2010 21:50:26 +0900 Cezary Kaliszyk FSet: definition changes propagated from Nominal and more use of 'descending' tactic changeset | files
(0) -30000 -10000 -1024 +1024 +10000 +30000 tip
isabelle