src/HOL/HOL.thy
2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-12-15 haftmann 2010-12-15 simplified evaluation function names
2010-12-07 blanchet 2010-12-07 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
2010-12-06 haftmann 2010-12-06 moved bootstrap of type_lifting to Fun
2010-12-06 haftmann 2010-12-06 replace `type_mapper` by the more adequate `type_lifting`
2010-12-03 wenzelm 2010-12-03 setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
2010-12-01 haftmann 2010-12-01 merged
2010-12-01 haftmann 2010-12-01 file for package tool type_mapper carries the same name as its Isar command
2010-12-01 wenzelm 2010-12-01 simplified HOL.eq simproc matching;
2010-11-26 wenzelm 2010-11-26 lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately;
2010-11-17 haftmann 2010-11-17 module for functorial mappers
2010-10-27 blanchet 2010-10-27 reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
2010-09-29 krauss 2010-09-29 backed out my old attempt at single_hyp_subst_tac (67cd6ed76446) It never was totally reliable, and better alternatives now exist (Subgoal.FOCUS).
2010-09-27 blanchet 2010-09-27 merged
2010-09-27 blanchet 2010-09-27 comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
2010-09-27 haftmann 2010-09-27 corrected OCaml operator precedence
2010-09-20 haftmann 2010-09-20 Pure equality is a regular cpde operation
2010-09-16 haftmann 2010-09-16 adjusted to changes in Code_Runtime
2010-09-15 wenzelm 2010-09-15 dropped obsolete src/Tools/random_word.ML -- superseded by src/Tools/Metis/src/Random.sml stemming from the Metis distribution;
2010-09-15 haftmann 2010-09-15 introduced "holds" as synthetic datatype constructor for "prop"; moved Pure code generator setup to Code_Generator.thy
2010-09-15 haftmann 2010-09-15 Code_Runtime.value, corresponding to ML_Context.value
2010-09-15 haftmann 2010-09-15 code_eval renamed to code_runtime
2010-09-15 haftmann 2010-09-15 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
2010-09-11 blanchet 2010-09-11 added Auto Try to the mix of automatic tools
2010-09-10 haftmann 2010-09-10 Haskell == is infix, not infixl
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-09-02 blanchet 2010-09-02 merged
2010-09-02 blanchet 2010-09-02 use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this *really* speeds up things -- HOL now builds 12% faster on my machine
2010-09-02 haftmann 2010-09-02 merged
2010-09-02 haftmann 2010-09-02 avoid cyclic modules
2010-09-02 haftmann 2010-09-02 merged
2010-09-02 haftmann 2010-09-02 normalization is allowed to solve True
2010-09-02 blanchet 2010-09-02 merged
2010-09-02 blanchet 2010-09-02 merged
2010-09-01 blanchet 2010-09-01 finish moving file
2010-09-02 haftmann 2010-09-02 normalization fails on unchanged goal
2010-09-01 haftmann 2010-09-01 tuned text segment
2010-08-31 blanchet 2010-08-31 fiddling with "try"
2010-08-30 haftmann 2010-08-30 hide all-too-popular constant name eq
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-08-26 haftmann 2010-08-26 prevent line breaks after Scala symbolic operators
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-25 wenzelm 2010-08-25 discontinued obsolete 'global' and 'local' commands;
2010-08-23 haftmann 2010-08-23 refined and unified naming convention for dynamic code evaluation techniques
2010-08-19 haftmann 2010-08-19 deglobalized named HOL constants
2010-08-19 haftmann 2010-08-19 tuned declaration order
2010-08-18 haftmann 2010-08-18 qualified constants Let and If
2010-07-19 haftmann 2010-07-19 optional break
2010-07-12 wenzelm 2010-07-12 moved misc legacy stuff from OldGoals to Misc_Legacy; OldGoals: removed unused strip_context, metahyps_thms, read_term, read_prop, gethyps;
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-06-15 haftmann 2010-06-15 added code_simp infrastructure
2010-06-14 haftmann 2010-06-14 dropped unused bindings
2010-06-01 blanchet 2010-06-01 removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-15 wenzelm 2010-05-15 incorporated further conversions and conversionals, after some minor tuning;
2010-05-09 wenzelm 2010-05-09 just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)