Fri, 02 Apr 2004 17:28:16 +0200 fixed dpll solver (now uses NNF)
webertj [Fri, 02 Apr 2004 17:28:16 +0200] rev 14514
fixed dpll solver (now uses NNF)
Fri, 02 Apr 2004 17:26:00 +0200 - Experimental command for instantiation of locales in proof contexts:
ballarin [Fri, 02 Apr 2004 17:26:00 +0200] rev 14513
- Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>
Fri, 02 Apr 2004 17:06:15 +0200 variable renamings and other cosmetic changes
paulson [Fri, 02 Apr 2004 17:06:15 +0200] rev 14512
variable renamings and other cosmetic changes
Fri, 02 Apr 2004 16:21:57 +0200 updated treatment of znegative and nat_of
paulson [Fri, 02 Apr 2004 16:21:57 +0200] rev 14511
updated treatment of znegative and nat_of
Fri, 02 Apr 2004 14:48:31 +0200 introduced fast_arith_neq_limit
nipkow [Fri, 02 Apr 2004 14:48:31 +0200] rev 14510
introduced fast_arith_neq_limit
Fri, 02 Apr 2004 14:47:11 +0200 got rid of ignore_neq again.
nipkow [Fri, 02 Apr 2004 14:47:11 +0200] rev 14509
got rid of ignore_neq again.
Fri, 02 Apr 2004 14:08:30 +0200 Experimental command for instantiation of locales in proof contexts:
ballarin [Fri, 02 Apr 2004 14:08:30 +0200] rev 14508
Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>
Fri, 02 Apr 2004 12:25:48 +0200 ignore_neq also influences arith_tac now, not just fast_arith_tac
nipkow [Fri, 02 Apr 2004 12:25:48 +0200] rev 14507
ignore_neq also influences arith_tac now, not just fast_arith_tac
Fri, 02 Apr 2004 12:08:38 +0200 Added ignore_neq flag.
nipkow [Fri, 02 Apr 2004 12:08:38 +0200] rev 14506
Added ignore_neq flag.
Thu, 01 Apr 2004 15:05:04 +0200 removal of Binary Trees examples prepratory to its going into AFP
paulson [Thu, 01 Apr 2004 15:05:04 +0200] rev 14505
removal of Binary Trees examples prepratory to its going into AFP
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip