| Mon, 20 Jul 2009 15:24:31 +0200 | haftmann | merged | changeset | files |
| Mon, 20 Jul 2009 15:24:15 +0200 | haftmann | less digestible | changeset | files |
| Mon, 20 Jul 2009 11:47:17 +0200 | haftmann | refined outline structure | changeset | files |
| Mon, 20 Jul 2009 19:57:32 +0200 | wenzelm | replaced usedir option -Q by more fine-grained -q; | changeset | files |
| Mon, 20 Jul 2009 13:52:27 +0200 | wenzelm | merged | changeset | files |
| Mon, 20 Jul 2009 09:52:09 +0200 | haftmann | merged | changeset | files |
| Mon, 20 Jul 2009 08:31:12 +0200 | haftmann | closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text | changeset | files |
| Wed, 15 Jul 2009 16:00:06 +0200 | haftmann | merged | changeset | files |
| Mon, 20 Jul 2009 08:32:07 +0200 | haftmann | merged | changeset | files |
| Wed, 15 Jul 2009 18:20:08 +0200 | haftmann | simplification of locale interfaces | changeset | files |
| Wed, 15 Jul 2009 10:11:13 +0200 | haftmann | additional preprocessor rule | changeset | files |
| Tue, 14 Jul 2009 16:27:34 +0200 | haftmann | added code_unfold_post attribute | changeset | files |
| Tue, 14 Jul 2009 16:27:33 +0200 | haftmann | more accessors to unfold simpset | changeset | files |
| Tue, 14 Jul 2009 16:27:33 +0200 | haftmann | clarified code | changeset | files |
| Tue, 14 Jul 2009 16:27:32 +0200 | haftmann | prefer code_inline over code_unfold; use code_unfold_post where appropriate | changeset | files |
| Tue, 14 Jul 2009 16:27:31 +0200 | haftmann | tuned code annotations | changeset | files |
| Tue, 14 Jul 2009 16:27:30 +0200 | haftmann | more canonical import | changeset | files |
| Tue, 14 Jul 2009 15:55:27 +0200 | haftmann | merged | changeset | files |
| Tue, 14 Jul 2009 15:54:51 +0200 | haftmann | merged | changeset | files |
| Tue, 14 Jul 2009 15:54:19 +0200 | haftmann | refinement of lattice classes | changeset | files |
| Mon, 13 Jul 2009 08:25:43 +0200 | haftmann | removed outdated comment | changeset | files |
| Mon, 20 Jul 2009 00:37:39 +0200 | wenzelm | Proof.future_proof: declare all assumptions as well; | changeset | files |
| Sun, 19 Jul 2009 19:24:04 +0200 | wenzelm | parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs; | changeset | files |
| Sun, 19 Jul 2009 19:20:17 +0200 | wenzelm | cancel_proofs: some attempts at reworking group management (based on body promises only); | changeset | files |
| Sun, 19 Jul 2009 18:42:05 +0200 | wenzelm | support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies); | changeset | files |
| Sun, 19 Jul 2009 18:02:40 +0200 | wenzelm | more abstract Future.is_worker; | changeset | files |
| Sun, 19 Jul 2009 17:08:34 +0200 | wenzelm | tuned; | changeset | files |
| Sun, 19 Jul 2009 14:15:47 +0200 | wenzelm | future_result: explicitly impose Variable.sorts_of again; | changeset | files |
| Sun, 19 Jul 2009 14:14:25 +0200 | wenzelm | recovered a version of dequeue_towards (cf. bb7b5a5942c7); | changeset | files |
| Sat, 18 Jul 2009 22:53:02 +0200 | wenzelm | added join_bodies; | changeset | files |
| Sat, 18 Jul 2009 22:52:31 +0200 | wenzelm | scheduler: tuned tracing (status); | changeset | files |
| Sat, 18 Jul 2009 22:51:29 +0200 | wenzelm | added group_id; | changeset | files |
| Sat, 18 Jul 2009 22:45:33 +0200 | wenzelm | synchronized: tuned tracing; | changeset | files |
| Sat, 18 Jul 2009 00:34:22 +0200 | wenzelm | tuned; | changeset | files |
| Sat, 18 Jul 2009 00:33:57 +0200 | wenzelm | tuned prf_subst: use structure Same; | changeset | files |
| Fri, 17 Jul 2009 23:13:57 +0200 | wenzelm | merged | changeset | files |
| Fri, 17 Jul 2009 13:12:18 -0400 | avigad | Changed fact_Suc_nat back to fact_Suc | changeset | files |
| Fri, 17 Jul 2009 23:13:50 +0200 | wenzelm | merged | changeset | files |
| Fri, 17 Jul 2009 10:07:15 +0200 | berghofe | merged | changeset | files |
| Wed, 15 Jul 2009 15:09:56 +0200 | berghofe | merged | changeset | files |
| Tue, 14 Jul 2009 21:19:34 -0400 | avigad | commit merge | changeset | files |
| Tue, 14 Jul 2009 20:58:53 -0400 | avigad | Repairs regarding new Fact.thy. | changeset | files |
| Tue, 14 Jul 2009 17:20:02 +0200 | berghofe | merged | changeset | files |
| Tue, 14 Jul 2009 17:18:51 +0200 | berghofe | merged | changeset | files |
| Tue, 14 Jul 2009 17:17:37 +0200 | berghofe | Use term antiquotation to refer to constant names in subsection title. | changeset | files |
| Fri, 10 Jul 2009 12:55:06 -0400 | avigad | Repaired uses of factorial. | changeset | files |
| Fri, 10 Jul 2009 10:45:49 -0400 | avigad | Automated merge with http://isabelle.in.tum.de/repos/isabelle | changeset | files |
| Fri, 10 Jul 2009 10:45:30 -0400 | avigad | Moved factorial lemmas from Binomial.thy to Fact.thy and merged. | changeset | files |
| Fri, 17 Jul 2009 23:11:40 +0200 | wenzelm | tuned/modernized Envir.subst_XXX; | changeset | files |
| Fri, 17 Jul 2009 22:54:11 +0200 | wenzelm | tuned/modernized subst: Same.operation; | changeset | files |
| Fri, 17 Jul 2009 22:51:18 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 17 Jul 2009 21:33:00 +0200 | wenzelm | tuned/modernized Envir operations; | changeset | files |
| Fri, 17 Jul 2009 21:33:00 +0200 | wenzelm | major cleanup, simplification, modernization; | changeset | files |
| Fri, 17 Jul 2009 21:32:59 +0200 | wenzelm | eq_type: special case for empty environment; | changeset | files |
| Fri, 17 Jul 2009 21:32:58 +0200 | wenzelm | compare types directly -- no need to invoke Type.eq_type with empty environment; | changeset | files |
| Thu, 16 Jul 2009 23:12:12 +0200 | wenzelm | incr_indexes (from Proofterm); | changeset | files |
| Thu, 16 Jul 2009 22:58:45 +0200 | wenzelm | tuned incr_indexes; | changeset | files |
| Thu, 16 Jul 2009 22:58:07 +0200 | wenzelm | tuned incr_tvar_same; | changeset | files |
| Thu, 16 Jul 2009 22:54:39 +0200 | wenzelm | added same; | changeset | files |
| Thu, 16 Jul 2009 22:22:03 +0200 | wenzelm | tuned map_proof_terms_option; | changeset | files |
| Thu, 16 Jul 2009 21:29:02 +0200 | wenzelm | export incr_tvar_same; | changeset | files |
| Thu, 16 Jul 2009 21:28:39 +0200 | wenzelm | added map_option; | changeset | files |
| Thu, 16 Jul 2009 21:28:09 +0200 | wenzelm | use structure Same; | changeset | files |
| Thu, 16 Jul 2009 21:00:09 +0200 | wenzelm | use structure Same; | changeset | files |
| Thu, 16 Jul 2009 20:32:40 +0200 | wenzelm | use structure Same; | changeset | files |
| Thu, 16 Jul 2009 20:32:05 +0200 | wenzelm | use structure Same; | changeset | files |
| Thu, 16 Jul 2009 20:15:57 +0200 | wenzelm | added map; | changeset | files |
| Thu, 16 Jul 2009 17:03:11 +0200 | wenzelm | use structure Same; | changeset | files |
| Thu, 16 Jul 2009 16:24:49 +0200 | wenzelm | Support for copy-avoiding functions on pure values, at the cost of readability. | changeset | files |
| Thu, 16 Jul 2009 00:24:11 +0200 | wenzelm | removed obsolete/unused legacy_varify; | changeset | files |
| Thu, 16 Jul 2009 00:21:36 +0200 | wenzelm | eliminated legacy_varify; | changeset | files |
| Wed, 15 Jul 2009 23:50:40 +0200 | wenzelm | merged | changeset | files |
| Wed, 15 Jul 2009 22:30:27 +0200 | Christian Urban | simplified proofs | changeset | files |
| Wed, 15 Jul 2009 23:48:21 +0200 | wenzelm | more antiquotations; | changeset | files |
| Wed, 15 Jul 2009 23:11:57 +0200 | wenzelm | eliminated obsolete legacy_varify; | changeset | files |
| Wed, 15 Jul 2009 21:42:24 +0200 | wenzelm | tuned comment; | changeset | files |
| Wed, 15 Jul 2009 20:34:58 +0200 | nipkow | Made "prime" executable | changeset | files |
| Wed, 15 Jul 2009 15:09:33 +0200 | nipkow | More finite set induction rules | changeset | files |
| Wed, 15 Jul 2009 12:44:41 +0200 | nipkow | made upt/upto executable on nat/int by simp | changeset | files |
| Tue, 14 Jul 2009 12:18:52 +0200 | wenzelm | removed obsolete/unused legacy_unvarify; | changeset | files |
| Tue, 14 Jul 2009 12:10:44 +0200 | wenzelm | tuned prepare_patternT: Term.exists_subtype; | changeset | files |
| Tue, 14 Jul 2009 12:10:01 +0200 | wenzelm | tuned paramify_vars: Term_Subst.map_atypsT_option; | changeset | files |
| Tue, 14 Jul 2009 10:56:43 +0200 | haftmann | merged | changeset | files |
| Tue, 14 Jul 2009 10:54:54 +0200 | haftmann | updated to changes in sources; tuned | changeset | files |
| Tue, 14 Jul 2009 10:54:21 +0200 | haftmann | updated to changes in sources; tuned | changeset | files |
| Tue, 14 Jul 2009 10:54:04 +0200 | haftmann | code attributes use common underscore convention | changeset | files |
| Tue, 14 Jul 2009 10:53:44 +0200 | haftmann | NEWS and CONTRIBUTORS | changeset | files |
| Mon, 13 Jul 2009 19:07:05 +0200 | berghofe | Tuned proof of lcm_1_iff_int, because metis produced enormous proof term. | changeset | files |
| Sun, 12 Jul 2009 14:48:01 +0200 | nipkow | more gcd/lcm lemmas | changeset | files |
| Sun, 12 Jul 2009 11:36:09 +0200 | nipkow | typo | changeset | files |
| Sun, 12 Jul 2009 11:25:56 +0200 | nipkow | resolvd conflict | changeset | files |
| Sun, 12 Jul 2009 10:14:51 +0200 | nipkow | More about gcd/lcm, and some cleaning up | changeset | files |
| Sat, 11 Jul 2009 21:33:01 +0200 | haftmann | added boolean_algebra type class; tuned lattice duals | changeset | files |
| Fri, 10 Jul 2009 09:24:50 +0200 | krauss | move Kleene_Algebra to Library | changeset | files |
| Fri, 10 Jul 2009 07:59:44 +0200 | haftmann | merged | changeset | files |
| Fri, 10 Jul 2009 07:59:29 +0200 | haftmann | tuned locale interface | changeset | files |
| Fri, 10 Jul 2009 07:59:28 +0200 | haftmann | tuned | changeset | files |
| Fri, 10 Jul 2009 07:59:27 +0200 | haftmann | dropped find_index_eq | changeset | files |
| Fri, 10 Jul 2009 07:59:25 +0200 | haftmann | tuned quickcheck generator for bool | changeset | files |
| Fri, 10 Jul 2009 07:59:23 +0200 | haftmann | tuned | changeset | files |
| Fri, 10 Jul 2009 00:49:32 +0200 | wenzelm | merged | changeset | files |
| Fri, 10 Jul 2009 00:10:36 +0200 | wenzelm | merged | changeset | files |
| Fri, 10 Jul 2009 00:47:17 +0200 | wenzelm | tuned varify/unvarify: use Term_Subst.map_XXX combinators; | changeset | files |
| Fri, 10 Jul 2009 00:08:38 +0200 | wenzelm | added some generic mapping combinators; | changeset | files |
| Thu, 09 Jul 2009 23:05:59 +0200 | krauss | reorganised; many new lemmas thanks to sledgehammer | changeset | files |
| Thu, 09 Jul 2009 23:05:59 +0200 | krauss | tuned | changeset | files |
| Thu, 09 Jul 2009 22:48:12 +0200 | wenzelm | renamed structure TermSubst to Term_Subst; | changeset | files |
| Thu, 09 Jul 2009 22:36:11 +0200 | wenzelm | Sorttab in Pure; | changeset | files |
| Thu, 09 Jul 2009 22:13:19 +0200 | wenzelm | removed obsolete CVS Ids; | changeset | files |
| Thu, 09 Jul 2009 22:09:58 +0200 | wenzelm | removed obsolete CVS Ids; | changeset | files |
| Thu, 09 Jul 2009 22:04:10 +0200 | wenzelm | merged | changeset | files |
| Thu, 09 Jul 2009 22:02:24 +0200 | wenzelm | recovered some proofs broken in 0314441a53a6; | changeset | files |
| Thu, 09 Jul 2009 22:01:41 +0200 | wenzelm | renamed functor TableFun to Table, and GraphFun to Graph; | changeset | files |
| Thu, 09 Jul 2009 17:34:59 +0200 | krauss | move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure | changeset | files |
| Thu, 09 Jul 2009 17:33:22 +0200 | krauss | drop unused lemmas | changeset | files |
| Thu, 09 Jul 2009 10:34:51 +0200 | chaieb | FPS form a metric space, which justifies the infinte sum notation | changeset | files |
| Thu, 09 Jul 2009 08:55:42 +0200 | chaieb | merged | changeset | files |
| Sun, 05 Jul 2009 21:10:23 +0200 | chaieb | merged | changeset | files |
| Sat, 04 Jul 2009 15:19:47 +0200 | chaieb | merged | changeset | files |
| Sat, 04 Jul 2009 15:19:29 +0200 | chaieb | merged | changeset | files |
| Thu, 02 Jul 2009 13:48:39 +0200 | chaieb | Gettring rid of sorts hyps | changeset | files |
| Wed, 08 Jul 2009 08:18:07 +0200 | haftmann | tuned structure Code internally | changeset | files |
| Wed, 08 Jul 2009 06:43:30 +0200 | nipkow | merged | changeset | files |
| Wed, 08 Jul 2009 06:42:35 +0200 | nipkow | name fixed | changeset | files |
| Tue, 07 Jul 2009 21:26:08 +0200 | haftmann | merged | changeset | files |
| Tue, 07 Jul 2009 17:50:03 +0200 | haftmann | merged | changeset | files |
| Tue, 07 Jul 2009 17:21:27 +0200 | haftmann | tuned interface of structure Code | changeset | files |
| Tue, 07 Jul 2009 17:21:26 +0200 | haftmann | more accurate certificates for constant aliasses | changeset | files |
| Tue, 07 Jul 2009 21:24:55 +0200 | haftmann | merged | changeset | files |
| Tue, 07 Jul 2009 17:37:00 +0200 | haftmann | Stefan Berghofer's code generator uses Pure equality instead of HOL equality now | changeset | files |
| Tue, 07 Jul 2009 20:16:06 +0200 | wenzelm | fixed proof (cf. 40501bb2d57c); | changeset | files |
| Tue, 07 Jul 2009 17:39:51 +0200 | nipkow | renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int | changeset | files |
| Tue, 07 Jul 2009 07:56:24 +0200 | haftmann | merged | changeset | files |
| Mon, 06 Jul 2009 16:49:51 +0200 | haftmann | tuned code | changeset | files |
| Mon, 06 Jul 2009 14:19:13 +0200 | haftmann | moved Inductive.myinv to Fun.inv; tuned | changeset | files |
| Tue, 07 Jul 2009 00:29:34 +0200 | wenzelm | add_classrel/arity: strip_shyps of stored result; | changeset | files |
| Mon, 06 Jul 2009 22:42:27 +0200 | wenzelm | clarified strip_shyps: proper type witnesses for present sorts; | changeset | files |
| Mon, 06 Jul 2009 22:41:00 +0200 | wenzelm | witness_sorts: proper type witnesses for hyps, not invented "'hyp" variables; | changeset | files |
| Mon, 06 Jul 2009 21:24:30 +0200 | wenzelm | structure Thm: less pervasive names; | changeset | files |
| Mon, 06 Jul 2009 20:36:38 +0200 | wenzelm | clarified Thm.of_class/of_sort/class_triv; | changeset | files |
| Mon, 06 Jul 2009 19:58:52 +0200 | wenzelm | renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort; | changeset | files |
| Sat, 04 Jul 2009 23:25:28 +0200 | wenzelm | renamed Delay to Swing_Thread.delay (action is executed within AWT thread!); | changeset | files |
| Sat, 04 Jul 2009 22:22:34 +0200 | wenzelm | Delayed action. | changeset | files |
| Sat, 04 Jul 2009 12:40:57 +0200 | wenzelm | merged | changeset | files |
| Sat, 04 Jul 2009 07:58:34 +0200 | haftmann | merged | changeset | files |
| Fri, 03 Jul 2009 23:29:03 +0200 | haftmann | nominal.ML is nominal_datatype.ML | changeset | files |
| Fri, 03 Jul 2009 16:51:56 +0200 | haftmann | merged | changeset | files |
| Fri, 03 Jul 2009 16:51:08 +0200 | haftmann | nominal.ML is nominal_datatype.ML | changeset | files |
| Fri, 03 Jul 2009 16:51:07 +0200 | haftmann | cleaned up fundamental iml term functions; nested patterns | changeset | files |
| Fri, 03 Jul 2009 16:51:07 +0200 | haftmann | cleaned up fundamental iml term functions | changeset | files |
| Fri, 03 Jul 2009 16:51:06 +0200 | haftmann | proper closures -- imperative programming considered harmful... | changeset | files |
| Fri, 03 Jul 2009 16:51:06 +0200 | haftmann | avoid useless code equations | changeset | files |
| Fri, 03 Jul 2009 08:51:34 +0200 | haftmann | restored subscripts | changeset | files |
| Fri, 03 Jul 2009 08:44:13 +0200 | haftmann | lemma foldl_apply_inv | changeset | files |
| Sat, 04 Jul 2009 11:46:51 +0200 | wenzelm | is_open: surrogate sequence is High..Low; | changeset | files |
| Fri, 03 Jul 2009 21:14:46 +0200 | wenzelm | init/check Isabelle_System; | changeset | files |
| Fri, 03 Jul 2009 21:14:16 +0200 | wenzelm | init isabelle home from existing setting or hint via system property; | changeset | files |
| Fri, 03 Jul 2009 20:37:14 +0200 | wenzelm | more hgignore; | changeset | files |
| Fri, 03 Jul 2009 16:36:02 +0200 | wenzelm | basic setup for Isabelle/JVM application bundle; | changeset | files |
| Fri, 03 Jul 2009 16:10:49 +0200 | wenzelm | separate setup for App1; | changeset | files |
| Fri, 03 Jul 2009 10:54:26 +0200 | wenzelm | SCALA_HOME: proper line escapes for choosefrom; | changeset | files |
| Fri, 03 Jul 2009 00:15:59 +0200 | wenzelm | allow reloading of settings within JVM process; | changeset | files |
| Fri, 03 Jul 2009 00:10:19 +0200 | wenzelm | Isabelle application wrapper for windows. | changeset | files |
| Fri, 03 Jul 2009 00:06:40 +0200 | wenzelm | isabelle.home: native jvmpath; | changeset | files |
| Fri, 03 Jul 2009 00:02:07 +0200 | wenzelm | Generic Isabelle application wrapper. | changeset | files |
| Fri, 03 Jul 2009 00:00:03 +0200 | wenzelm | observe SCALA_HOME, if available; | changeset | files |
| Thu, 02 Jul 2009 22:18:02 +0200 | wenzelm | merged | changeset | files |
| Thu, 02 Jul 2009 21:24:32 +0200 | wenzelm | recovered subscripts, which were lost in b41d61c768e2 (due to Emacs accident?); | changeset | files |
| Thu, 02 Jul 2009 18:32:28 +0200 | haftmann | merged | changeset | files |
| Thu, 02 Jul 2009 16:06:12 +0200 | haftmann | instance arities can be simultaneous | changeset | files |
| Thu, 02 Jul 2009 16:00:28 +0200 | haftmann | updated generated files | changeset | files |
| Thu, 02 Jul 2009 16:00:27 +0200 | haftmann | more friendly wrt. PGs interpretation of compound *); added dedicated section on value and quickcheck | changeset | files |
| Thu, 02 Jul 2009 14:43:06 +0100 | paulson | merged | changeset | files |
| Thu, 02 Jul 2009 10:49:46 +0100 | paulson | Deleted some debugging code | changeset | files |
| Wed, 01 Jul 2009 16:19:44 +0100 | paulson | merged | changeset | files |
| Wed, 24 Jun 2009 16:28:30 +0100 | paulson | merged | changeset | files |
| Tue, 23 Jun 2009 15:48:55 +0100 | paulson | merged | changeset | files |
| Thu, 18 Jun 2009 17:14:08 +0100 | paulson | Removed unnecessary conditions concerning nonzero divisors | changeset | files |
| Thu, 02 Jul 2009 22:17:08 +0200 | wenzelm | strip_shyps: remove top sort, which is logically insignificant; | changeset | files |
| Thu, 02 Jul 2009 21:26:18 +0200 | wenzelm | renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML); | changeset | files |
| Thu, 02 Jul 2009 20:55:44 +0200 | wenzelm | added pro-forma proof constructor Inclass; | changeset | files |
| Thu, 02 Jul 2009 17:34:14 +0200 | wenzelm | renamed NamedThmsFun to Named_Thms; | changeset | files |
| Thu, 02 Jul 2009 17:33:36 +0200 | wenzelm | renamed NamedThmsFun to Named_Thms; | changeset | files |
| Thu, 02 Jul 2009 17:30:54 +0200 | wenzelm | misc tuning; | changeset | files |
| Thu, 02 Jul 2009 15:37:22 +0200 | wenzelm | fixed document (DERIV_intros); | changeset | files |
| Tue, 30 Jun 2009 22:23:33 +0200 | wenzelm | more detailed timing message; | changeset | files |
| Tue, 30 Jun 2009 22:12:46 +0200 | wenzelm | default to maximum max_threads; | changeset | files |
| Tue, 30 Jun 2009 22:05:07 +0200 | wenzelm | merged | changeset | files |
| Tue, 30 Jun 2009 22:04:41 +0200 | wenzelm | fixed ISABELLE_HOME_USER; | changeset | files |
| Tue, 30 Jun 2009 22:03:40 +0200 | haftmann | merged | changeset | files |
| Tue, 30 Jun 2009 19:45:52 +0200 | haftmann | adaptated to changes in term representation | changeset | files |
| Tue, 30 Jun 2009 19:31:50 +0200 | haftmann | improved treatment of case patterns | changeset | files |
| Tue, 30 Jun 2009 18:24:03 +0200 | haftmann | merged | changeset | files |
| Tue, 30 Jun 2009 18:23:50 +0200 | haftmann | an intermediate step towards a refined translation of cases | changeset | files |
| Tue, 30 Jun 2009 17:33:30 +0200 | haftmann | all variable names are optional | changeset | files |
| Tue, 30 Jun 2009 16:43:28 +0200 | haftmann | variable names in abstractions are optional | changeset | files |
| Tue, 30 Jun 2009 16:43:27 +0200 | haftmann | restored | changeset | files |
| Tue, 30 Jun 2009 21:51:44 +0200 | wenzelm | added isatest for x86_64-darwin; | changeset | files |
| Tue, 30 Jun 2009 21:23:01 +0200 | wenzelm | merged | changeset | files |
| Tue, 30 Jun 2009 19:54:04 +0200 | hoelzl | NEWS updated | changeset | files |
| Tue, 30 Jun 2009 18:25:55 +0200 | hoelzl | DERIV_ln is proved in Transcendental and in Ln, use Transcendental to prove Ln. | changeset | files |
| Tue, 30 Jun 2009 18:24:00 +0200 | hoelzl | remove DERIV_tac and deriv_tac, neither is used in Isabelle/HOL or the AFP | changeset | files |
| Tue, 30 Jun 2009 18:21:55 +0200 | hoelzl | use DERIV_intros | changeset | files |
| Tue, 30 Jun 2009 18:16:22 +0200 | hoelzl | Added DERIV_intros | changeset | files |
| Tue, 30 Jun 2009 15:58:12 +0200 | bulwahn | commented trancl example; added debug message | changeset | files |
| Tue, 30 Jun 2009 14:55:06 +0200 | bulwahn | merged | changeset | files |
| Tue, 30 Jun 2009 14:54:30 +0200 | bulwahn | exported is_registered; added debug messages; removed extended parameter compilation in predicate compiler | changeset | files |
| Mon, 29 Jun 2009 12:33:58 +0200 | bulwahn | added diagnostic printing; changed proof for parameters; moved code | changeset | files |
| Tue, 30 Jun 2009 14:54:32 +0200 | haftmann | merged | changeset | files |
| Tue, 30 Jun 2009 14:54:00 +0200 | haftmann | simplified binding concept | changeset | files |
| Tue, 30 Jun 2009 14:53:59 +0200 | haftmann | temporary workaround | changeset | files |
| Tue, 30 Jun 2009 14:53:58 +0200 | haftmann | tuned | changeset | files |
| Tue, 30 Jun 2009 14:53:57 +0200 | haftmann | streamlined code | changeset | files |
| Tue, 30 Jun 2009 14:53:56 +0200 | haftmann | dropped id | changeset | files |
| Mon, 29 Jun 2009 16:17:57 +0200 | haftmann | mutual instances | changeset | files |
| Mon, 29 Jun 2009 16:17:56 +0200 | haftmann | canonical prefix for datatype derivates | changeset | files |
| Mon, 29 Jun 2009 16:17:55 +0200 | haftmann | tuned | changeset | files |
| Tue, 30 Jun 2009 11:21:02 +0200 | immler | check for correct proof output | changeset | files |
| Tue, 30 Jun 2009 11:21:02 +0200 | immler | fixed: count constants with supplementary lemmas | changeset | files |
| Tue, 30 Jun 2009 10:59:02 +0200 | hoelzl | removed latex markup - there is no document generated from Decision_Procs/ex | changeset | files |
| Mon, 29 Jun 2009 23:29:11 +0200 | hoelzl | Implemented taylor series expansion for approximation | changeset | files |
| Tue, 30 Jun 2009 21:19:32 +0200 | wenzelm | renamed Swing to Swing_Thread, to avoid overlap with scala.swing.Swing; | changeset | files |
| Tue, 30 Jun 2009 00:57:24 +0200 | wenzelm | merged | changeset | files |
| Tue, 30 Jun 2009 00:50:42 +0200 | wenzelm | more display; | changeset | files |
| Tue, 30 Jun 2009 00:57:06 +0200 | wenzelm | added icon; | changeset | files |
| Tue, 30 Jun 2009 00:46:28 +0200 | wenzelm | basic launch4j setup; | changeset | files |
| Tue, 30 Jun 2009 00:31:18 +0200 | wenzelm | fixed permissions; | changeset | files |
| Tue, 30 Jun 2009 00:14:30 +0200 | wenzelm | fixed permissions; | changeset | files |
| Mon, 29 Jun 2009 20:05:44 +0200 | berghofe | Corrected handling of bound variables. | changeset | files |
| Mon, 29 Jun 2009 14:55:08 +0200 | haftmann | merged | changeset | files |
| Mon, 29 Jun 2009 12:18:58 +0200 | haftmann | dropped Id | changeset | files |
| Mon, 29 Jun 2009 12:18:57 +0200 | haftmann | explicit Set constructor for code generated for sets | changeset | files |
| Mon, 29 Jun 2009 12:18:57 +0200 | haftmann | hide popular names | changeset | files |
| Mon, 29 Jun 2009 12:18:56 +0200 | haftmann | Executable_Set is now a simple wrapper around Fset | changeset | files |
| Mon, 29 Jun 2009 12:18:55 +0200 | haftmann | renamed theory Code_Set to Fset | changeset | files |
| Mon, 29 Jun 2009 12:18:54 +0200 | haftmann | updated generated document | changeset | files |
| Sun, 28 Jun 2009 11:02:27 +0200 | haftmann | Executable_Set now based on Code_Set | changeset | files |
| Sun, 28 Jun 2009 10:33:36 +0200 | haftmann | added Inter, Union | changeset | files |
| Sun, 28 Jun 2009 22:51:29 +0200 | wenzelm | more precise dependencies for "jars"; | changeset | files |
| Sun, 28 Jun 2009 22:50:37 +0200 | wenzelm | improved display; | changeset | files |