src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
17 months ago haftmann 2018-04-24 proper datatype for 8-bit characters
20 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
21 months ago wenzelm 2017-11-26 more symbols;
2016-09-26 haftmann 2016-09-26 syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div
2016-09-01 wenzelm 2016-09-01 tuned headers;
2016-03-12 haftmann 2016-03-12 model characters directly as range 0..255 * * * operate on syntax terms rather than asts
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-15 Andreas Lochbihler 2015-09-15 avoid module dependency cycles
2015-09-09 Andreas Lochbihler 2015-09-09 reactivate examples with predicate compiler and quickcheck
2015-09-06 haftmann 2015-09-06 prefer "uncurry" as canonical name for case distinction on products in combinatorial view
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-04-13 hoelzl 2015-04-13 predicate compiler: ignore Abs_filter and Rep_filter
2014-04-24 blanchet 2014-04-24 avoid name shadowing
2014-03-13 nipkow 2014-03-13 enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2012-08-01 wenzelm 2012-08-01 fixed document;
2012-04-30 bulwahn 2012-04-30 removing obsolete setup for sets now that sets are executable
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-03-13 wenzelm 2012-03-13 prefer abs_def over def_raw;
2012-03-12 noschinl 2012-03-12 tuned proofs
2011-12-24 haftmann 2011-12-24 adjusted to set/pred distinction by means of type constructor `set`
2011-11-11 bulwahn 2011-11-11 using more conventional names for monad plus operations
2011-10-21 bulwahn 2011-10-21 replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2010-12-08 haftmann 2010-12-08 primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
2010-11-15 bulwahn 2010-11-15 ignoring the constant STR in the predicate compiler
2010-10-21 bulwahn 2010-10-21 adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
2010-09-23 bulwahn 2010-09-23 handling equivalences smarter in the predicate compiler
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-06-28 haftmann 2010-06-28 merged constants "split" and "prod_case"
2010-04-21 bulwahn 2010-04-21 added further inlining of boolean constants to the predicate compiler
2010-04-21 bulwahn 2010-04-21 added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
2010-03-31 bulwahn 2010-03-31 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
2010-03-24 bulwahn 2010-03-24 moved further predicate compile files to HOL-Library