| Fri, 02 Apr 2004 16:21:57 +0200 |
paulson |
updated treatment of znegative and nat_of
|
changeset |
files
|
| Fri, 02 Apr 2004 14:48:31 +0200 |
nipkow |
introduced fast_arith_neq_limit
|
changeset |
files
|
| Fri, 02 Apr 2004 14:47:11 +0200 |
nipkow |
got rid of ignore_neq again.
|
changeset |
files
|
| Fri, 02 Apr 2004 14:08:30 +0200 |
ballarin |
Experimental command for instantiation of locales in proof contexts:
|
changeset |
files
|
| Fri, 02 Apr 2004 12:25:48 +0200 |
nipkow |
ignore_neq also influences arith_tac now, not just fast_arith_tac
|
changeset |
files
|
| Fri, 02 Apr 2004 12:08:38 +0200 |
nipkow |
Added ignore_neq flag.
|
changeset |
files
|
| Thu, 01 Apr 2004 15:05:04 +0200 |
paulson |
removal of Binary Trees examples prepratory to its going into AFP
|
changeset |
files
|
| Thu, 01 Apr 2004 10:54:32 +0200 |
paulson |
new type class abelian_group
|
changeset |
files
|
| Wed, 31 Mar 2004 16:10:53 +0200 |
skalberg |
Added check that Theory.ML does not occur in the files section of the theory
|
changeset |
files
|
| Wed, 31 Mar 2004 11:02:00 +0200 |
nipkow |
Lex now in AFP
|
changeset |
files
|
| Wed, 31 Mar 2004 11:00:25 +0200 |
nipkow |
HOL/Lex is now in AFP/Functional-Automata
|
changeset |
files
|
| Wed, 31 Mar 2004 10:51:50 +0200 |
streckem |
new
|
changeset |
files
|
| Tue, 30 Mar 2004 19:33:57 +0200 |
streckem |
new
|
changeset |
files
|
| Tue, 30 Mar 2004 19:28:27 +0200 |
streckem |
Added PSV 2003/2004
|
changeset |
files
|
| Tue, 30 Mar 2004 11:25:14 +0200 |
paulson |
tidied
|
changeset |
files
|
| Tue, 30 Mar 2004 11:18:12 +0200 |
paulson |
tidied
|
changeset |
files
|