Wed, 07 May 2008 10:59:54 +0200 Updated.
berghofe [Wed, 07 May 2008 10:59:54 +0200] rev 26839
Updated.
Wed, 07 May 2008 10:59:53 +0200 Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma
berghofe [Wed, 07 May 2008 10:59:53 +0200] rev 26838
Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma to avoid problems with HO unification.
Wed, 07 May 2008 10:59:52 +0200 Replaced instance declarations for sets by instance declarations for bool.
berghofe [Wed, 07 May 2008 10:59:52 +0200] rev 26837
Replaced instance declarations for sets by instance declarations for bool. Together with the instance declarations for fun from Ffun, this subsumes the old instance declarations for sets.
Wed, 07 May 2008 10:59:51 +0200 Adm now imports Ffun rather than Cont, because SetPcpo, which imports Adm,
berghofe [Wed, 07 May 2008 10:59:51 +0200] rev 26836
Adm now imports Ffun rather than Cont, because SetPcpo, which imports Adm, needs functions (since sets are now just functions).
Wed, 07 May 2008 10:59:50 +0200 Lookup and union operations on terms are now modulo eta conversion.
berghofe [Wed, 07 May 2008 10:59:50 +0200] rev 26835
Lookup and union operations on terms are now modulo eta conversion.
Wed, 07 May 2008 10:59:49 +0200 Terms returned by decomp are now eta-contracted.
berghofe [Wed, 07 May 2008 10:59:49 +0200] rev 26834
Terms returned by decomp are now eta-contracted.
Wed, 07 May 2008 10:59:48 +0200 Added function for computing instantiation for the subst rule, which is used
berghofe [Wed, 07 May 2008 10:59:48 +0200] rev 26833
Added function for computing instantiation for the subst rule, which is used in vars_gen_hyp_subst_tac and blast_hyp_subst_tac to avoid problems with HO unification.
Wed, 07 May 2008 10:59:47 +0200 eq_assumption now uses aeconv instead of aconv.
berghofe [Wed, 07 May 2008 10:59:47 +0200] rev 26832
eq_assumption now uses aeconv instead of aconv.
Wed, 07 May 2008 10:59:46 +0200 - Removed function eta_contract_atom, which did not quite work
berghofe [Wed, 07 May 2008 10:59:46 +0200] rev 26831
- Removed function eta_contract_atom, which did not quite work - Corrected and simplified function aeconv
Wed, 07 May 2008 10:59:45 +0200 Replaced Pattern.eta_contract_atom by Envir.eta_contract.
berghofe [Wed, 07 May 2008 10:59:45 +0200] rev 26830
Replaced Pattern.eta_contract_atom by Envir.eta_contract.
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip