paulson [Wed, 23 Sep 2009 11:05:28 +0100] rev 32648
Correct chasing of type variable instantiations during type unification.
The following theory should not raise exception TERM:
constdefs
somepredicate :: "(('b => 'b) => ('a => 'a))
=> 'a => 'b => bool"
"somepredicate upd v x == True"
lemma somepredicate_idI:
"somepredicate id (f v) v"
by (simp add: somepredicate_def)
lemma somepredicate_triv:
"somepredicate upd v x ==> somepredicate upd v x"
by assumption
lemmas somepredicate_triv [OF somepredicate_idI]
lemmas st' = somepredicate_triv[where v="h :: nat => bool"]
lemmas st2 = st'[OF somepredicate_idI]
haftmann [Wed, 23 Sep 2009 11:33:52 +0200] rev 32647
hide newly introduced constants
Philipp Meyer [Tue, 22 Sep 2009 11:26:46 +0200] rev 32646
used standard fold function and type aliases
Philipp Meyer [Mon, 21 Sep 2009 15:05:26 +0200] rev 32645
sos method generates and uses proof certificates
wenzelm [Tue, 22 Sep 2009 20:25:31 +0200] rev 32644
full reserve of worker threads -- for improved CPU utilization;
haftmann [Tue, 22 Sep 2009 15:38:12 +0200] rev 32643
merged
haftmann [Tue, 22 Sep 2009 15:36:55 +0200] rev 32642
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer