| Sat, 15 Mar 2014 08:31:33 +0100 |
haftmann |
more complete set of lemmas wrt. image and composition
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 08:56:08 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 22:45:09 +0100 |
haftmann |
bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 22:30:58 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 16 Jan 2014 16:50:41 +0100 |
blanchet |
moved lemmas from 'Fun_More_FP' to where they belong
|
file |
diff |
annotate
|
| Mon, 25 Nov 2013 10:14:29 +0100 |
traytel |
eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:20 +0200 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 15:50:33 +0200 |
Andreas Lochbihler |
add lemmas
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:16:07 +0200 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Wed, 03 Apr 2013 10:15:43 +0200 |
haftmann |
generalized lemma fold_image thanks to Peter Lammich
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 09:19:37 +0200 |
haftmann |
simp results for simplification results of Inf/Sup expressions on bool;
|
file |
diff |
annotate
|
| Mon, 08 Oct 2012 12:03:49 +0200 |
haftmann |
consolidated names of theorems on composition;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 10:49:47 +0200 |
huffman |
tuned lemmas (v)image_id;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2012 20:51:07 +0200 |
haftmann |
centralized enriched_type declaration, thanks to in-situ available Isar commands
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Wed, 22 Feb 2012 08:05:28 +0100 |
bulwahn |
generalizing inj_on_Int
|
file |
diff |
annotate
|
| Sun, 05 Feb 2012 08:47:13 +0100 |
bulwahn |
removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)
|
file |
diff |
annotate
|
| Sun, 05 Feb 2012 08:36:41 +0100 |
bulwahn |
adding a remark about lemma which is too special and should be removed
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 20:26:13 +0100 |
wenzelm |
explicit is better than implicit;
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:20 +0200 |
bulwahn |
removing old code generator setup for function types
|
file |
diff |
annotate
|
| Wed, 14 Sep 2011 10:08:52 -0400 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Sat, 10 Sep 2011 10:29:24 +0200 |
haftmann |
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 14:25:16 +0200 |
nipkow |
added new lemmas
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:25:17 +0200 |
haftmann |
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
|
file |
diff |
annotate
|
| Wed, 27 Jul 2011 19:34:30 +0200 |
hoelzl |
finite vimage on arbitrary domains
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 22:25:14 +0200 |
haftmann |
more on complement
|
file |
diff |
annotate
|
| Thu, 07 Jul 2011 21:53:53 +0200 |
nipkow |
added translation to fix critical pair between abbreviations for surj and ~=
|
file |
diff |
annotate
|
| Fri, 20 May 2011 21:38:32 +0200 |
hoelzl |
add surj_vimage_empty
|
file |
diff |
annotate
|
| Tue, 05 Apr 2011 11:44:34 +0200 |
blanchet |
added "no_atp" to Cantor's paradox
|
file |
diff |
annotate
|
| Fri, 21 Jan 2011 09:44:12 +0100 |
haftmann |
moved theorem
|
file |
diff |
annotate
|
| Tue, 11 Jan 2011 14:12:37 +0100 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:43:54 +0100 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:25:05 +0100 |
haftmann |
moved bootstrap of type_lifting to Fun
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:19:10 +0100 |
haftmann |
replace `type_mapper` by the more adequate `type_lifting`
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 21:09:36 +0100 |
wenzelm |
keep private things private, without comments;
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 14:14:17 +0100 |
hoelzl |
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 10:34:33 +0100 |
hoelzl |
Replace surj by abbreviation; remove surj_on.
|
file |
diff |
annotate
|
| Thu, 18 Nov 2010 17:01:15 +0100 |
haftmann |
map_fun combinator in theory Fun
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 10:45:55 +0200 |
nipkow |
put expand_(fun/set)_eq back in as synonyms, for compatibility
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 21:08:31 +0200 |
hoelzl |
Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 11:54:09 +0200 |
hoelzl |
Introduce surj_on and replace surj and bij by abbreviations.
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 10:45:51 +0200 |
hoelzl |
Permutation implies bij function
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 10:36:45 +0200 |
hoelzl |
bij <--> bij_betw
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 17:46:55 +0200 |
haftmann |
inj_comp and inj_fun
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Fri, 09 Jul 2010 08:11:10 +0200 |
haftmann |
nicer xsymbol syntax for fcomp and scomp
|
file |
diff |
annotate
|
| 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
|
| 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
|