src/Pure/Proof/proofchecker.ML
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Thu, 03 Jun 2010 23:56:05 +0200 wenzelm do not open Proofterm, which is very ould style;
Tue, 01 Jun 2010 10:53:55 +0200 berghofe - Equality check on propositions after lookup of theorem now takes type variable
Tue, 30 Mar 2010 15:25:30 +0200 krauss switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
Sat, 27 Mar 2010 15:20:31 +0100 wenzelm moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Fri, 27 Feb 2009 16:38:52 +0100 wenzelm eliminated NJ's List.nth;
Wed, 31 Dec 2008 19:54:04 +0100 wenzelm Term.declare_term_frees;
Wed, 31 Dec 2008 18:53:16 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Sat, 15 Nov 2008 21:31:32 +0100 wenzelm adapted PThm;
Thu, 23 Oct 2008 15:28:01 +0200 wenzelm renamed Thm.get_axiom_i to Thm.axiom;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Thu, 10 May 2007 00:39:56 +0200 wenzelm moved conversions to structure Conv;
Tue, 05 Dec 2006 00:30:38 +0100 wenzelm thm/prf: separate official name vs. additional tags;
Wed, 19 Jul 2006 12:12:07 +0200 wenzelm thm_of_proof: improved generation of variables;
Tue, 18 Jul 2006 20:01:47 +0200 wenzelm thm_of_proof: tuned Name operations;
Tue, 11 Jul 2006 12:16:54 +0200 wenzelm replaced Term.variant(list) by Name.variant(_list);
Wed, 09 Nov 2005 16:26:41 +0100 wenzelm Thm.varifyT': natural argument order;
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Thu, 01 Sep 2005 22:15:10 +0200 wenzelm curried_lookup/update;
Fri, 15 Jul 2005 15:44:17 +0200 wenzelm tuned;
Wed, 29 Jun 2005 15:13:38 +0200 wenzelm Drule.implies_intr_hyps;
Thu, 09 Jun 2005 12:03:38 +0200 wenzelm PureThy.all_thms_of;
Thu, 21 Apr 2005 19:13:03 +0200 berghofe Adapted to new interface of instantiation and unification / matching functions.
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Wed, 23 Jun 2004 14:44:22 +0200 skalberg Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Wed, 27 Nov 2002 17:25:04 +0100 berghofe - tuned beta_eta_convert
Mon, 21 Oct 2002 17:20:29 +0200 berghofe Fixed problem with theorems containing TFrees.
Mon, 19 Nov 2001 17:40:45 +0100 berghofe Improved error message.
Fri, 28 Sep 2001 11:04:44 +0200 berghofe Exchanged % and %%.
Fri, 31 Aug 2001 18:46:48 +0200 wenzelm tuned headers;
Fri, 31 Aug 2001 16:17:05 +0200 berghofe Initial revision of tools for proof terms.
less more (0) tip