| Tue, 18 Nov 2008 18:25:52 +0100 |
wenzelm |
added force_proofs;
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 23:17:13 +0100 |
wenzelm |
tuned promise/fullfill;
|
file |
diff |
annotate
|
| Sun, 16 Nov 2008 22:12:43 +0100 |
wenzelm |
put_name/thm_proof: promises are filled with fulfilled proofs;
|
file |
diff |
annotate
|
| Sun, 16 Nov 2008 20:03:42 +0100 |
wenzelm |
clarified Thm.proof_body_of vs. Thm.proof_of;
|
file |
diff |
annotate
|
| Sat, 15 Nov 2008 21:31:25 +0100 |
wenzelm |
refined notion of derivation, consiting of promises and proof_body;
|
file |
diff |
annotate
|
| Thu, 23 Oct 2008 15:28:05 +0200 |
wenzelm |
renamed get_axiom_i to axiom, removed obsolete get_axiom;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2008 16:53:10 +0200 |
wenzelm |
join results in isolation;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:33 +0200 |
wenzelm |
added weaken_sorts;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 12:18:18 +0200 |
wenzelm |
renamed promise to future, tuned related interfaces;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 12:00:00 +0200 |
wenzelm |
more precise join_futures, improved termination;
|
file |
diff |
annotate
|
| Tue, 30 Sep 2008 22:02:44 +0200 |
wenzelm |
export explicit joint_futures, removed Theory.at_end hook;
|
file |
diff |
annotate
|
| Sun, 28 Sep 2008 12:42:35 +0200 |
wenzelm |
join earlier promises first;
|
file |
diff |
annotate
|
| Sun, 28 Sep 2008 12:23:44 +0200 |
wenzelm |
promise_result: enforce strictly sequential dependencies, via serial numbers;
|
file |
diff |
annotate
|
| Sat, 27 Sep 2008 18:18:05 +0200 |
wenzelm |
Future.release_results;
|
file |
diff |
annotate
|
| Sat, 27 Sep 2008 15:20:37 +0200 |
wenzelm |
promise: include check into future body, i.e. joined results are always valid;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 20:34:19 +0200 |
wenzelm |
simplified promise;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 14:35:02 +0200 |
wenzelm |
abtract types: plain datatype with opaque signature matching;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 13:21:13 +0200 |
wenzelm |
explicit type OrdList.T;
|
file |
diff |
annotate
|
| Tue, 23 Sep 2008 15:48:52 +0200 |
wenzelm |
added dest_deriv, removed external type deriv;
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 15:26:14 +0200 |
wenzelm |
type thm: fully internal derivation, no longer exported;
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 19:39:44 +0200 |
wenzelm |
simplified oracle interface;
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 14:06:56 +0200 |
wenzelm |
added deriv.ML: Abstract derivations based on raw proof terms.
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 23:45:49 +0200 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:59:47 +0200 |
berghofe |
eq_assumption now uses aeconv instead of aconv.
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 18:49:19 +0200 |
wenzelm |
Theory.eq_thy;
|
file |
diff |
annotate
|
| Sun, 13 Apr 2008 16:40:06 +0200 |
wenzelm |
simplified handling of sorts, removed unnecessary universal witness;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:45 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:09 +0100 |
wenzelm |
eliminated theory ProtoPure;
|
file |
diff |
annotate
|