Tue, 26 Sep 2006 13:34:35 +0200 handling of \<^const> syntax for case; explicit case names for induction rules for rep_datatype
haftmann [Tue, 26 Sep 2006 13:34:35 +0200] rev 20715
handling of \<^const> syntax for case; explicit case names for induction rules for rep_datatype
Tue, 26 Sep 2006 13:34:17 +0200 tuned syntax for <= <
haftmann [Tue, 26 Sep 2006 13:34:17 +0200] rev 20714
tuned syntax for <= <
Tue, 26 Sep 2006 13:34:16 +0200 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
haftmann [Tue, 26 Sep 2006 13:34:16 +0200] rev 20713
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
Tue, 26 Sep 2006 13:34:15 +0200 renamed 0 and 1 to HOL.zero and HOL.one respectivly
haftmann [Tue, 26 Sep 2006 13:34:15 +0200] rev 20712
renamed 0 and 1 to HOL.zero and HOL.one respectivly
Tue, 26 Sep 2006 11:11:57 +0200 fixed the definition of "depth"
paulson [Tue, 26 Sep 2006 11:11:57 +0200] rev 20711
fixed the definition of "depth"
Tue, 26 Sep 2006 11:09:33 +0200 Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
paulson [Tue, 26 Sep 2006 11:09:33 +0200] rev 20710
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
(0) -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip