| Thu, 22 Oct 2009 09:27:48 +0200 |
nipkow |
inv_onto -> inv_into
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:32:51 +0100 |
paulson |
Some new lemmas concerning sets
|
file |
diff |
annotate
|
| Mon, 19 Oct 2009 16:43:45 +0200 |
berghofe |
Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).
|
file |
diff |
annotate
|
| Sun, 18 Oct 2009 12:07:25 +0200 |
nipkow |
Inv -> inv_onto, inv abbr. inv_onto UNIV.
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 13:46:39 +0200 |
nipkow |
added the_inv_onto
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 10 Sep 2009 15:23:07 +0200 |
haftmann |
early bootstrap of generic transfer procedure
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 17:00:41 +0200 |
nipkow |
new lemma bij_comp
|
file |
diff |
annotate
|
| Wed, 22 Jul 2009 18:02:10 +0200 |
haftmann |
moved complete_lattice &c. into separate theory
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 14:19:13 +0200 |
haftmann |
moved Inductive.myinv to Fun.inv; tuned
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 15:04:33 +0200 |
haftmann |
separate directory for datatype package
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 13:26:32 +0200 |
nipkow |
A few finite lemmas
|
file |
diff |
annotate
|
| Tue, 19 May 2009 13:57:31 +0200 |
haftmann |
pretty printing of functional combinators for evaluation code
|
file |
diff |
annotate
|
| Sat, 09 May 2009 07:25:22 +0200 |
nipkow |
lemmas by Andreas Lochbihler
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 08:23:08 +0100 |
haftmann |
dropped Id
|
file |
diff |
annotate
|
| Fri, 31 Oct 2008 10:35:30 +0100 |
berghofe |
Replaced arbitrary by undefined.
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 23:45:39 +0200 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
file |
diff |
annotate
|
| Fri, 13 Jun 2008 15:22:07 +0200 |
nipkow |
hide -> hide (open)
|
file |
diff |
annotate
|
| Thu, 12 Jun 2008 14:10:41 +0200 |
nipkow |
Hid swap
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 19:15:18 +0200 |
wenzelm |
tuned proofs -- case_tac *is* available here;
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:56 +0200 |
haftmann |
removed some dubious code lemmas
|
file |
diff |
annotate
|
| Wed, 09 Apr 2008 08:10:11 +0200 |
haftmann |
removed syntax from monad combinators; renamed mbind to scomp
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 12:04:53 +0100 |
haftmann |
added forward composition
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:50:42 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 20:38:12 +0100 |
haftmann |
moved some set lemmas to Set.thy
|
file |
diff |
annotate
|
| Thu, 21 Feb 2008 17:33:58 +0100 |
nipkow |
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
|
file |
diff |
annotate
|
| Thu, 10 Jan 2008 19:10:08 +0100 |
berghofe |
Added test data generator for function type (from Pure/codegen.ML).
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 20:40:19 +0200 |
wenzelm |
simproc_setup fun_upd2;
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:27:56 +0200 |
haftmann |
simplified HOL bootstrap
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:02:07 +0200 |
berghofe |
Added ML bindings for sup_fun_eq and sup_bool_eq.
|
file |
diff |
annotate
|
| Wed, 09 May 2007 07:53:06 +0200 |
haftmann |
moved recfun_codegen.ML to Code_Generator.thy
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 00:10:59 +0200 |
wenzelm |
ML antiquotes;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 21:32:09 +0100 |
haftmann |
moved lattice instance here
|
file |
diff |
annotate
|
| Wed, 27 Dec 2006 19:09:55 +0100 |
haftmann |
explizit serialization for Haskell id
|
file |
diff |
annotate
|
| Mon, 18 Dec 2006 08:21:26 +0100 |
haftmann |
infix syntax for generated code for composition
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 13:42:39 +0100 |
haftmann |
moved order arities for fun and bool to Fun/Orderings
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 15:43:04 +0100 |
haftmann |
dropped Typedef dependency
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:30 +0200 |
wenzelm |
simprocs: no theory argument -- use simpset context instead;
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:01 +0200 |
wenzelm |
tuned concrete syntax -- abbreviation/const_syntax;
|
file |
diff |
annotate
|
| Tue, 02 May 2006 20:42:32 +0200 |
wenzelm |
replaced syntax/translations by abbreviation;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:06 +0200 |
wenzelm |
refined 'abbreviation';
|
file |
diff |
annotate
|
| Thu, 23 Mar 2006 20:03:53 +0100 |
nipkow |
Converted translations to abbbreviations.
|
file |
diff |
annotate
|
| Fri, 11 Nov 2005 00:09:37 +0100 |
huffman |
add header
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:34 +0200 |
wenzelm |
Goal.prove;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:15 +0200 |
wenzelm |
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 23:56:15 +0200 |
nipkow |
renamed rules to iprover
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 15:36:28 +0200 |
paulson |
classical rules must have names for ATP integration
|
file |
diff |
annotate
|
| Mon, 01 Aug 2005 19:20:26 +0200 |
wenzelm |
simprocs: Simplifier.inherit_bounds;
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
| Sun, 10 Apr 2005 17:19:03 +0200 |
nipkow |
_(_|_) is now override_on
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Wed, 09 Feb 2005 18:32:28 +0100 |
paulson |
new foldSet proofs
|
file |
diff |
annotate
|
| Fri, 14 Jan 2005 12:00:27 +0100 |
nipkow |
made diff_less a simp rule
|
file |
diff |
annotate
|
| Sun, 21 Nov 2004 15:44:20 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Wed, 04 Aug 2004 19:11:02 +0200 |
nipkow |
added some inj_on thms
|
file |
diff |
annotate
|
| Wed, 14 Apr 2004 14:13:05 +0200 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
| Mon, 14 Apr 2003 18:52:13 +0200 |
nipkow |
Added thms
|
file |
diff |
annotate
|
| Thu, 10 Oct 2002 14:21:20 +0200 |
berghofe |
- Added range_ex1_eq
|
file |
diff |
annotate
|
| Thu, 26 Sep 2002 10:51:29 +0200 |
paulson |
Converted Fun to Isar style.
|
file |
diff |
annotate
|
| Tue, 11 Dec 2001 13:43:00 +0100 |
wenzelm |
oops;
|
file |
diff |
annotate
|
| Mon, 10 Dec 2001 20:59:43 +0100 |
wenzelm |
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Wed, 21 Nov 2001 00:33:40 +0100 |
wenzelm |
got rid of theory Inverse_Image;
|
file |
diff |
annotate
|
| Fri, 09 Nov 2001 00:09:47 +0100 |
wenzelm |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file |
diff |
annotate
|
| Thu, 27 Sep 2001 22:28:16 +0200 |
wenzelm |
eliminated theories "equalities" and "mono" (made part of "Typedef",
|
file |
diff |
annotate
|
| Wed, 25 Jul 2001 13:13:01 +0200 |
paulson |
partial restructuring to reduce dependence on Axiom of Choice
|
file |
diff |
annotate
|
| Wed, 14 Feb 2001 20:45:35 +0100 |
oheimb |
removed whitespace
|
file |
diff |
annotate
|
| Mon, 08 Jan 2001 12:27:36 +0100 |
nipkow |
Removed Applyall
|
file |
diff |
annotate
|
| Thu, 12 Oct 2000 18:38:23 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Sun, 16 Jul 2000 20:48:35 +0200 |
wenzelm |
syntax (symbols) "op o" moved from HOL to Fun;
|
file |
diff |
annotate
|
| Fri, 14 Jul 2000 16:27:45 +0200 |
oheimb |
added hint on fun_sum
|
file |
diff |
annotate
|
| Thu, 13 Jul 2000 23:08:42 +0200 |
wenzelm |
fixed compose decl;
|
file |
diff |
annotate
|
| Sun, 25 Jun 2000 23:58:27 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 24 May 2000 18:48:03 +0200 |
paulson |
we must not require SetInterval this early
|
file |
diff |
annotate
|
| Tue, 23 May 2000 07:32:24 +0200 |
nipkow |
Added SetInterval
|
file |
diff |
annotate
|
| Fri, 18 Feb 2000 20:24:16 +0100 |
oheimb |
changed precedence of function update
|
file |
diff |
annotate
|
| Fri, 27 Aug 1999 15:41:11 +0200 |
paulson |
the bij predicate (at last)
|
file |
diff |
annotate
|
| Wed, 03 Feb 1999 13:26:07 +0100 |
paulson |
inj is now a translation of inj_on
|
file |
diff |
annotate
|
| Fri, 13 Nov 1998 13:26:16 +0100 |
paulson |
the function space operator
|
file |
diff |
annotate
|
| Fri, 02 Oct 1998 14:28:39 +0200 |
nipkow |
id <-> Id
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 16:23:25 +0200 |
oheimb |
cleanup for Fun.thy:
|
file |
diff |
annotate
|
| Mon, 27 Apr 1998 16:45:11 +0200 |
nipkow |
Added a few lemmas.
|
file |
diff |
annotate
|
| Tue, 24 Feb 1998 11:35:33 +0100 |
paulson |
New theory of the inverse image of a function
|
file |
diff |
annotate
|
| Sat, 01 Nov 1997 12:59:06 +0100 |
paulson |
New Blast_tac (and minor tidying...)
|
file |
diff |
annotate
|
| Fri, 04 Apr 1997 16:33:28 +0200 |
nipkow |
moved inj and surj from Set to Fun and Inv -> inv.
|
file |
diff |
annotate
|
| Mon, 05 Feb 1996 21:27:16 +0100 |
clasohm |
expanded tabs; renamed subtype to typedef;
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:02:25 +0100 |
clasohm |
new version of HOL with curried function application
|
file |
diff |
annotate
|