src/HOL/Hyperreal/transfer.ML
Wed, 01 Aug 2007 19:59:12 +0200 huffman fix looping when applied to standard subgoals
Sun, 29 Jul 2007 14:29:54 +0200 wenzelm renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
Mon, 07 May 2007 00:49:59 +0200 wenzelm simplified DataFun interfaces;
Fri, 20 Apr 2007 11:21:37 +0200 haftmann transfer_tac accepts also HOL equations as theorems
Thu, 07 Dec 2006 23:16:55 +0100 wenzelm reorganized structure Tactic vs. MetaSimplifier;
Wed, 29 Nov 2006 15:44:51 +0100 wenzelm simplified method setup;
Thu, 23 Nov 2006 22:38:30 +0100 wenzelm prefer Proof.context over Context.generic;
Sat, 08 Jul 2006 12:54:37 +0200 wenzelm Goal.prove: context;
Sat, 27 May 2006 17:41:59 +0200 wenzelm unfold/refold: LocalDefs.meta_rewrite_rule;
Sat, 21 Jan 2006 23:02:20 +0100 wenzelm simplified type attribute;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Tue, 25 Oct 2005 18:18:49 +0200 wenzelm avoid legacy goals;
Fri, 21 Oct 2005 18:14:34 +0200 wenzelm Goal.prove;
Fri, 16 Sep 2005 01:42:57 +0200 huffman use mem operator
Thu, 15 Sep 2005 23:46:22 +0200 huffman merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
Mon, 12 Sep 2005 23:18:01 +0200 huffman add header
Mon, 12 Sep 2005 23:14:41 +0200 huffman added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
Mon, 12 Sep 2005 23:06:24 +0200 huffman new implementation of transfer principle
less more (0) tip