src/Pure/thm.ML
Tue, 18 Nov 2008 22:25:36 +0100 wenzelm fulfill_proof/thm_proof: commuted lazyness;
Tue, 18 Nov 2008 18:25:52 +0100 wenzelm added force_proofs;
Mon, 17 Nov 2008 23:17:13 +0100 wenzelm tuned promise/fullfill;
Sun, 16 Nov 2008 22:12:43 +0100 wenzelm put_name/thm_proof: promises are filled with fulfilled proofs;
Sun, 16 Nov 2008 20:03:42 +0100 wenzelm clarified Thm.proof_body_of vs. Thm.proof_of;
Sat, 15 Nov 2008 21:31:25 +0100 wenzelm refined notion of derivation, consiting of promises and proof_body;
Thu, 23 Oct 2008 15:28:05 +0200 wenzelm renamed get_axiom_i to axiom, removed obsolete get_axiom;
Tue, 21 Oct 2008 16:53:10 +0200 wenzelm join results in isolation;
Thu, 16 Oct 2008 22:44:33 +0200 wenzelm added weaken_sorts;
Wed, 01 Oct 2008 12:18:18 +0200 wenzelm renamed promise to future, tuned related interfaces;
Wed, 01 Oct 2008 12:00:00 +0200 wenzelm more precise join_futures, improved termination;
Tue, 30 Sep 2008 22:02:44 +0200 wenzelm export explicit joint_futures, removed Theory.at_end hook;
Sun, 28 Sep 2008 12:42:35 +0200 wenzelm join earlier promises first;
Sun, 28 Sep 2008 12:23:44 +0200 wenzelm promise_result: enforce strictly sequential dependencies, via serial numbers;
Sat, 27 Sep 2008 18:18:05 +0200 wenzelm Future.release_results;
Sat, 27 Sep 2008 15:20:37 +0200 wenzelm promise: include check into future body, i.e. joined results are always valid;
Thu, 25 Sep 2008 20:34:19 +0200 wenzelm simplified promise;
Thu, 25 Sep 2008 14:35:02 +0200 wenzelm abtract types: plain datatype with opaque signature matching;
Thu, 25 Sep 2008 13:21:13 +0200 wenzelm explicit type OrdList.T;
Tue, 23 Sep 2008 15:48:52 +0200 wenzelm added dest_deriv, removed external type deriv;
Mon, 22 Sep 2008 15:26:14 +0200 wenzelm type thm: fully internal derivation, no longer exported;
Thu, 18 Sep 2008 19:39:44 +0200 wenzelm simplified oracle interface;
Thu, 18 Sep 2008 14:06:56 +0200 wenzelm added deriv.ML: Abstract derivations based on raw proof terms.
Wed, 27 Aug 2008 11:48:54 +0200 wenzelm type Properties.T;
Mon, 23 Jun 2008 23:45:49 +0200 wenzelm Logic.all/mk_equals/mk_implies;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Wed, 07 May 2008 10:59:47 +0200 berghofe eq_assumption now uses aeconv instead of aconv.
Tue, 15 Apr 2008 18:49:19 +0200 wenzelm Theory.eq_thy;
Sun, 13 Apr 2008 16:40:06 +0200 wenzelm simplified handling of sorts, removed unnecessary universal witness;
Sat, 12 Apr 2008 17:00:45 +0200 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
Thu, 27 Mar 2008 14:41:09 +0100 wenzelm eliminated theory ProtoPure;
Mon, 21 Jan 2008 14:18:49 +0100 berghofe Removed Logic.auto_rename.
Thu, 04 Oct 2007 20:29:24 +0200 wenzelm replaced literal 'a by Name.aT;
Fri, 17 Aug 2007 23:10:45 +0200 wenzelm compress: proper check_thy;
Fri, 03 Aug 2007 16:28:22 +0200 wenzelm replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
Wed, 11 Jul 2007 11:59:21 +0200 berghofe Added function norm_proof for normalizing the proof term
Sun, 08 Jul 2007 19:52:05 +0200 wenzelm thm tag: Markup.property list;
Thu, 05 Jul 2007 20:01:38 +0200 wenzelm added type conv;
Mon, 25 Jun 2007 00:36:42 +0200 wenzelm added eta_long_conversion;
Fri, 08 Jun 2007 18:13:58 +0200 berghofe Adapted Proofterm.bicompose_proof to Larry's changes in
Thu, 31 May 2007 23:47:36 +0200 wenzelm simplified/unified list fold;
Thu, 10 May 2007 00:39:55 +0200 wenzelm added dest_fun/fun2/arg1;
Sat, 14 Apr 2007 17:36:17 +0200 wenzelm removed obsolete read_ctyp, read_def_cterm;
Wed, 04 Apr 2007 23:29:33 +0200 wenzelm rep_thm/cterm/ctyp: removed obsolete sign field;
Wed, 04 Apr 2007 00:11:16 +0200 wenzelm improved exception CTERM;
Tue, 03 Apr 2007 19:24:19 +0200 wenzelm avoid clash with Alice keywords;
Mon, 26 Feb 2007 23:18:30 +0100 wenzelm moved some non-kernel material to more_thm.ML;
Sun, 04 Feb 2007 22:02:17 +0100 wenzelm old-fashioned abstype ctyp/cterm/thm prevents accidental equality tests;
Tue, 02 Jan 2007 22:43:04 +0100 wenzelm Term.lambda: abstract over arbitrary closed terms;
Tue, 12 Dec 2006 20:49:25 +0100 wenzelm tuned error messages;
Tue, 05 Dec 2006 00:30:38 +0100 wenzelm thm/prf: separate official name vs. additional tags;
Wed, 29 Nov 2006 04:11:09 +0100 wenzelm simplified Logic.count_prems;
Tue, 21 Nov 2006 18:07:33 +0100 wenzelm moved theorem kinds from PureThy to Thm;
Sun, 05 Nov 2006 21:44:35 +0100 wenzelm removed obsolete first_duplicate;
Tue, 31 Oct 2006 09:29:06 +0100 haftmann fixed type signature of Type.varify
Wed, 11 Oct 2006 10:49:36 +0200 haftmann abandoned findrep
Sat, 07 Oct 2006 01:31:12 +0200 wenzelm added def_name_optional;
Sun, 01 Oct 2006 18:29:34 +0200 wenzelm cterm_match: avoid recalculation of maxidx;
Thu, 21 Sep 2006 19:05:31 +0200 wenzelm added dest_binop;
Mon, 18 Sep 2006 19:39:11 +0200 wenzelm added dest_arg, i.e. a tuned version of #2 o dest_comb;
less more (0) -300 -100 -60 tip