| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Fri, 05 Mar 2010 17:49:10 +0100 |
hoelzl |
generalized inj_uminus; added strict_mono_imp_inj_on
|
file |
diff |
annotate
|
| Thu, 04 Mar 2010 19:43:51 +0100 |
hoelzl |
Rewrite rules for images of minus of intervals
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2009 10:24:53 +0100 |
krauss |
killed a few warnings
|
file |
diff |
annotate
|
| Mon, 21 Dec 2009 08:32:22 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 21 Dec 2009 08:32:03 +0100 |
haftmann |
moved lemmas o_eq_dest, o_eq_elim here
|
file |
diff |
annotate
|
| Fri, 18 Dec 2009 18:48:27 -0800 |
huffman |
add lemma swap_triple
|
file |
diff |
annotate
|
| Wed, 16 Dec 2009 14:38:35 -0800 |
huffman |
declare swap_self [simp], add lemma comp_swap
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:41:36 +0100 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
| 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
|