2013-11-16 wenzelm 2013-11-16 proper thy_load command 'boogie_file' -- avoid direct access to file-system;
2013-11-16 wenzelm 2013-11-16 tuned signature;
2013-11-16 wenzelm 2013-11-16 updated example;
2013-11-16 wenzelm 2013-11-16 prefer UTF8.decode_permissive;
2013-11-16 wenzelm 2013-11-16 more distinctive Isabelle_Process.Output vs. Isabelle_Process.Protocol_Output;
2013-11-15 wenzelm 2013-11-15 more specific Protocol_Output: empty message.body, main content via bytes/text;
2013-11-14 wenzelm 2013-11-14 tuned imports;
2013-11-14 wenzelm 2013-11-14 tuned signature;
2013-11-14 wenzelm 2013-11-14 immutable byte vectors versus UTF8 strings;
2013-11-15 haftmann 2013-11-15 dropped duplicate of of_bool
2013-11-15 haftmann 2013-11-15 proper code equations for Gcd and Lcm on nat and int
2013-11-16 nipkow 2013-11-16 tuned
2013-11-14 blanchet 2013-11-14 fixed type variable confusion in 'datatype_new_compat'
2013-11-14 blanchet 2013-11-14 implemented 'tptp_translate'
2013-11-14 blanchet 2013-11-14 reintroduced (unimplemented) 'tptp_translate' tool
2013-11-14 blanchet 2013-11-14 have MaSh support nameless facts (i.e. proofs) and use that support
2013-11-14 blanchet 2013-11-14 made SML/NJ happy
2013-11-14 blanchet 2013-11-14 renamed thm
2013-11-14 haftmann 2013-11-14 explicit inclusion of data refinement theory into HOL-Library session
2013-11-14 nipkow 2013-11-14 tuned to improve automation (for REPEAT)
2013-11-13 haftmann 2013-11-13 separated comparision on bit operations into separate theory
2013-11-13 traytel 2013-11-13 prohibit locally fixed type variables in bnf definitions
2013-11-13 traytel 2013-11-13 tuned
2013-11-13 traytel 2013-11-13 standard relator for list bnf
2013-11-13 traytel 2013-11-13 tuned example
2013-11-13 blanchet 2013-11-13 shortened generated property name
2013-11-13 traytel 2013-11-13 more explicit syntax for defining a bnf
2013-11-13 hoelzl 2013-11-13 fix document generation for HOL-Probability
2013-11-12 hoelzl 2013-11-12 fix document generation for Extended_Nat
2013-11-12 hoelzl 2013-11-12 measure of a countable union
2013-11-12 hoelzl 2013-11-12 add restrict_space measure
2013-11-12 hoelzl 2013-11-12 better support for enat and ereal conversions
2013-11-12 hoelzl 2013-11-12 enat is countable
2013-11-12 hoelzl 2013-11-12 add equalities for SUP and INF over constant functions
2013-11-12 hoelzl 2013-11-12 add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
2013-11-12 hoelzl 2013-11-12 add acyclicI_order
2013-11-12 hoelzl 2013-11-12 stronger inc_induct and dec_induct
2013-11-12 hoelzl 2013-11-12 countability of the image of a reflexive transitive closure
2013-11-12 hoelzl 2013-11-12 support of_rat with 0 or 1 on order relations
2013-11-12 hoelzl 2013-11-12 equation when indicator function equals 0 or 1
2013-11-12 blanchet 2013-11-12 ported part of function package to new 'Ctr_Sugar' abstraction
2013-11-12 blanchet 2013-11-12 undid copy-paste
2013-11-12 blanchet 2013-11-12 ported 'partial_function' to 'Ctr_Sugar' abstraction
2013-11-12 blanchet 2013-11-12 port list comprehension simproc to 'Ctr_Sugar' abstraction
2013-11-12 blanchet 2013-11-12 added convenience function
2013-11-12 blanchet 2013-11-12 document idiomatic use of 'simps_of_case'
2013-11-12 blanchet 2013-11-12 ported 'Simps_Case_Conv' to use new 'Ctr_Sugar' abstraction
2013-11-12 blanchet 2013-11-12 register old-style datatypes as 'Ctr_Sugar'
2013-11-12 blanchet 2013-11-12 export useful ML function
2013-11-12 blanchet 2013-11-12 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
2013-11-12 blanchet 2013-11-12 tuned headers
2013-11-12 blanchet 2013-11-12 moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction
2013-11-12 wenzelm 2013-11-12 updated sessions;
2013-11-12 wenzelm 2013-11-12 proper latex -- NB: cannot use antiquotation here;
2013-11-11 wenzelm 2013-11-11 merged
2013-11-11 wenzelm 2013-11-11 simplified App template;
2013-11-11 wenzelm 2013-11-11 obsolete;
2013-11-11 wenzelm 2013-11-11 obsolete;
2013-11-11 wenzelm 2013-11-11 tuned message;
2013-11-11 wenzelm 2013-11-11 tuned signature -- removed obsolete Addsimprocs, Delsimprocs;