#
ec8d5b30 |
|
10-Nov-2018 |
haftmann <none@none> |
clarified status of legacy input abbreviations
|
#
cc47ae18 |
|
17-Jun-2018 |
nipkow <none@none> |
added simp rules
|
#
afc89de9 |
|
20-Apr-2018 |
haftmann <none@none> |
moved lemma to more appropriate place
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
#
daac7840 |
|
07-Aug-2017 |
blanchet <none@none> |
tuning imports
|
#
2df4ddef |
|
10-Aug-2016 |
nipkow <none@none> |
"split add" -> "split"
|
#
48473ab7 |
|
22-Jun-2016 |
wenzelm <none@none> |
bundle lifting_syntax;
|
#
aa5fce1c |
|
31-May-2016 |
eberlm <none@none> |
Added code generation for PMFs
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
3487f527 |
|
11-Nov-2015 |
Andreas Lochbihler <none@none> |
add various lemmas
|
#
372a4c7a |
|
31-Aug-2015 |
wenzelm <none@none> |
proper qualified naming;
|
#
f8b6675d |
|
31-Aug-2015 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
44dc7454 |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
more transfer rules
|
#
577a545f |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
add lemmas about functions on option
|
#
8bec0997 |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
tuned proof
|
#
23571538 |
|
07-Nov-2014 |
traytel <none@none> |
more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories
|
#
65fddcc1 |
|
04-Nov-2014 |
lammich <lammich@in.tum.de> |
Added Option.bind_split{,_asm,s}
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
#
ecb6646e |
|
02-Sep-2014 |
blanchet <none@none> |
tuned imports
|
#
2326a269 |
|
01-Sep-2014 |
blanchet <none@none> |
renamed BNF theories --HG-- rename : src/HOL/BNF_Comp.thy => src/HOL/BNF_Composition.thy rename : src/HOL/BNF_FP_Base.thy => src/HOL/BNF_Fixpoint_Base.thy rename : src/HOL/BNF_GFP.thy => src/HOL/BNF_Greatest_Fixpoint.thy rename : src/HOL/BNF_LFP.thy => src/HOL/BNF_Least_Fixpoint.thy
|
#
fb2f6a3a |
|
01-Sep-2014 |
blanchet <none@none> |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place --HG-- rename : src/HOL/Datatype.thy => src/HOL/Old_Datatype.thy rename : src/HOL/Tools/Function/size.ML => src/HOL/Tools/Function/old_size.ML rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Old_Datatype/old_datatype.ML rename : src/HOL/Tools/Datatype/datatype_aux.ML => src/HOL/Tools/Old_Datatype/old_datatype_aux.ML rename : src/HOL/Tools/Datatype/datatype_codegen.ML => src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML rename : src/HOL/Tools/Datatype/datatype_data.ML => src/HOL/Tools/Old_Datatype/old_datatype_data.ML rename : src/HOL/Tools/Datatype/datatype_prop.ML => src/HOL/Tools/Old_Datatype/old_datatype_prop.ML rename : src/HOL/Tools/Datatype/datatype_realizer.ML => src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML rename : src/HOL/Tools/Datatype/primrec.ML => src/HOL/Tools/Old_Datatype/old_primrec.ML rename : src/HOL/Tools/Datatype/rep_datatype.ML => src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
|
#
5a60fc1f |
|
29-May-2014 |
blanchet <none@none> |
tuned whitespace, to make datatype definitions slightly less intimidating
|
#
312f030c |
|
26-May-2014 |
blanchet <none@none> |
got rid of '=:' squiggly
|
#
a350d601 |
|
02-Mar-2014 |
blanchet <none@none> |
rationalized internals
|
#
a1d385ea |
|
17-Feb-2014 |
blanchet <none@none> |
renamed 'datatype_new_compat' to 'datatype_compat'
|
#
e91e0c03 |
|
16-Feb-2014 |
blanchet <none@none> |
folded 'Option.set' into BNF-generated 'set_option'
|
#
2f0985b8 |
|
13-Feb-2014 |
blanchet <none@none> |
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors) --HG-- rename : src/HOL/Tools/enriched_type.ML => src/HOL/Tools/functor.ML
|
#
447c00c8 |
|
13-Feb-2014 |
blanchet <none@none> |
merged 'Option.map' and 'Option.map_option'
|
#
80ec2685 |
|
12-Feb-2014 |
blanchet <none@none> |
tuning
|
#
aff8c6a4 |
|
12-Feb-2014 |
blanchet <none@none> |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
|
#
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
#
f7053da7 |
|
12-Feb-2014 |
blanchet <none@none> |
compatibility names
|
#
041d6368 |
|
12-Feb-2014 |
blanchet <none@none> |
use new selector support to define 'the', 'hd', 'tl'
|
#
0d093612 |
|
12-Feb-2014 |
blanchet <none@none> |
transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well) * * * compile * * * tuned imports to prevent merge issues in 'Main'
|
#
325c96bf |
|
24-Jan-2014 |
blanchet <none@none> |
killed 'More_BNFs' by moving its various bits where they (now) belong
|
#
9f589a46 |
|
20-Jan-2014 |
blanchet <none@none> |
swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
|
#
b0527b24 |
|
26-Sep-2013 |
lammich <lammich@in.tum.de> |
Added symmetric code_unfold-lemmas for null and is_none
|
#
0363b36f |
|
13-Aug-2013 |
kuncar <none@none> |
move useful lemmas to Main
|
#
a7b3de52 |
|
23-Jun-2013 |
haftmann <none@none> |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier --HG-- extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b
|
#
d8ea875e |
|
12-Apr-2013 |
wenzelm <none@none> |
modifiers for classical wrappers operate on Proof.context instead of claset;
|
#
27fdd5a0 |
|
13-Feb-2013 |
haftmann <none@none> |
combinator List.those; simprule for case distinction on Option.map expression
|
#
72ce2bac |
|
07-Sep-2012 |
haftmann <none@none> |
combinator Option.these
|
#
ba43f37d |
|
18-Feb-2012 |
krauss <none@none> |
added congruence rules for Option.{map|bind}
|
#
36c8d8b8 |
|
11-Jan-2011 |
haftmann <none@none> |
"enriched_type" replaces less specific "type_lifting" --HG-- rename : src/HOL/Tools/type_lifting.ML => src/HOL/Tools/enriched_type.ML
|
#
e8a2e703 |
|
21-Dec-2010 |
haftmann <none@none> |
tuned type_lifting declarations
|
#
14dbdf06 |
|
06-Dec-2010 |
haftmann <none@none> |
replace `type_mapper` by the more adequate `type_lifting` --HG-- rename : src/HOL/Tools/type_mapper.ML => src/HOL/Tools/type_lifting.ML
|
#
c5aa0f00 |
|
18-Nov-2010 |
haftmann <none@none> |
mapper for option type
|
#
40bdb407 |
|
10-Sep-2010 |
haftmann <none@none> |
Haskell == is infix, not infixl
|
#
27ff3609 |
|
06-Sep-2010 |
wenzelm <none@none> |
more antiquotations;
|
#
23399c25 |
|
05-Sep-2010 |
krauss <none@none> |
removed duplicate lemma
|
#
2bec7372 |
|
05-Sep-2010 |
krauss <none@none> |
added Option.bind
|
#
972f5d58 |
|
27-Aug-2010 |
haftmann <none@none> |
renamed class/constant eq to equal; tuned some instantiations
|
#
8c901cc8 |
|
19-Jul-2010 |
haftmann <none@none> |
Scala: subtle difference in printing strings vs. complex mixfix syntax
|
#
82fe7ca2 |
|
16-Apr-2010 |
wenzelm <none@none> |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
#
6abf497b |
|
10-Mar-2010 |
haftmann <none@none> |
split off theory Big_Operators from theory Finite_Set --HG-- rename : src/HOL/Finite_Set.thy => src/HOL/Big_Operators.thy
|
#
df118eed |
|
13-Jan-2010 |
haftmann <none@none> |
some syntax setup for Scala
|
#
5c2bc460 |
|
14-Jul-2009 |
haftmann <none@none> |
prefer code_inline over code_unfold; use code_unfold_post where appropriate
|
#
fbe41aef |
|
14-Jul-2009 |
haftmann <none@none> |
code attributes use common underscore convention
|
#
922dfe12 |
|
14-May-2009 |
haftmann <none@none> |
preprocessing must consider eq
|
#
6ca1bd25 |
|
08-May-2009 |
nipkow <none@none> |
lemmas by Andreas Lochbihler
|
#
08b8ac13 |
|
06-Mar-2009 |
haftmann <none@none> |
moved instance option :: finite to Option.thy
|
#
98a2ea1d |
|
04-Mar-2009 |
nipkow <none@none> |
Option.thy
|
#
61bc019f |
|
09-Aug-2007 |
haftmann <none@none> |
re-eliminated Option.thy
|
#
7d0fa4a2 |
|
07-Aug-2007 |
haftmann <none@none> |
split off Option theory
|
#
02dcaa23 |
|
21-Feb-2002 |
wenzelm <none@none> |
theory Option has been assimilated by Datatype;
|
#
4bf1375e |
|
30-May-2000 |
berghofe <none@none> |
the is now defined using primrec, avoiding explicit use of arbitrary.
|
#
b428c8de |
|
09-Sep-1998 |
oheimb <none@none> |
AddIffs[not_None_eq]; made wrapper ospec really safe
|
#
df41c559 |
|
24-Jul-1998 |
berghofe <none@none> |
Adapted to new datatype package.
|
#
83a33ab3 |
|
24-Mar-1998 |
oheimb <none@none> |
added o2s
|
#
3e1ccbfa |
|
10-Nov-1997 |
oheimb <none@none> |
replaced 8bit characters
|
#
43292bd8 |
|
04-Nov-1997 |
oheimb <none@none> |
added the, option_map, and case analysis theorems
|
#
d3e23685 |
|
24-Sep-1996 |
nipkow <none@none> |
Moved Option out of IOA into core HOL
|