Wed, 23 Sep 2009 13:47:08 +0200 Added "nitpick_const_simp" tags to lazy list theories.
blanchet [Wed, 23 Sep 2009 13:47:08 +0200] rev 32655
Added "nitpick_const_simp" tags to lazy list theories. (Will be useful once Nitpick is integrated in Isabelle.)
Wed, 23 Sep 2009 13:48:35 +0200 atbroy101 is long dead, use atbroy99; comment out broken SML test invocation
krauss [Wed, 23 Sep 2009 13:48:35 +0200] rev 32654
atbroy101 is long dead, use atbroy99; comment out broken SML test invocation
Wed, 23 Sep 2009 13:42:53 +0200 merged
haftmann [Wed, 23 Sep 2009 13:42:53 +0200] rev 32653
merged
Wed, 23 Sep 2009 12:03:47 +0200 stripped legacy ML bindings
haftmann [Wed, 23 Sep 2009 12:03:47 +0200] rev 32652
stripped legacy ML bindings
Wed, 23 Sep 2009 13:31:38 +0200 Undo errornous commit of Statespace change
hoelzl [Wed, 23 Sep 2009 13:31:38 +0200] rev 32651
Undo errornous commit of Statespace change
Wed, 23 Sep 2009 13:17:17 +0200 correct variable order in approximate-method
hoelzl [Wed, 23 Sep 2009 13:17:17 +0200] rev 32650
correct variable order in approximate-method
Wed, 23 Sep 2009 11:06:32 +0100 merged
paulson [Wed, 23 Sep 2009 11:06:32 +0100] rev 32649
merged
Wed, 23 Sep 2009 11:05:28 +0100 Correct chasing of type variable instantiations during type unification.
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]
Wed, 23 Sep 2009 11:33:52 +0200 hide newly introduced constants
haftmann [Wed, 23 Sep 2009 11:33:52 +0200] rev 32647
hide newly introduced constants
Tue, 22 Sep 2009 11:26:46 +0200 used standard fold function and type aliases
Philipp Meyer [Tue, 22 Sep 2009 11:26:46 +0200] rev 32646
used standard fold function and type aliases
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip