| Sun, 07 Mar 2010 12:19:47 +0100 |
modernized structure Object_Logic;
|
file | diff | annotate |
| Sat, 27 Feb 2010 23:13:01 +0100 |
modernized structure Term_Ord;
|
file | diff | annotate |
| Wed, 21 Oct 2009 00:36:12 +0200 |
standardized basic operations on type option;
|
file | diff | annotate |
| Tue, 28 Jul 2009 13:37:09 +0200 |
Set.UNIV and Set.empty are mere abbreviations for top and bot
|
file | diff | annotate |
| Wed, 11 Mar 2009 16:15:17 +0100 |
(restored previous version)
|
file | diff | annotate |
| Wed, 11 Mar 2009 15:56:51 +0100 |
HOLogic.mk_set, HOLogic.dest_set
|
file | diff | annotate |
| Thu, 05 Mar 2009 08:24:28 +0100 |
merged
|
file | diff | annotate |
| Thu, 05 Mar 2009 08:23:11 +0100 |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
file | diff | annotate |
| Fri, 27 Feb 2009 18:03:47 +0100 |
eliminated private clones of List.partition;
|
file | diff | annotate |
| Wed, 31 Dec 2008 15:30:10 +0100 |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file | diff | annotate |
| Wed, 31 Dec 2008 00:08:13 +0100 |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file | diff | annotate |
| Tue, 31 Jul 2007 09:31:26 +0200 |
find_body goes under meta-quantifier ; tactic generalizes free variables;
|
file | diff | annotate |
| Sun, 22 Jul 2007 17:53:54 +0200 |
Quantifier elimination for Dense linear orders after Langford
|
file | diff | annotate |