Mercurialisabelle / file revisions
summary | shortlog | changelog | graph | tags | branches | file | revisions | annotate | diff | rss
NEWS
2006-09-19 wenzelm 2006-09-19 * Pure: 'print_theory' now suppresses entities with internal name; file | diff | annotate
2006-09-19 haftmann 2006-09-19 Operational Equality file | diff | annotate
2006-09-18 wenzelm 2006-09-18 * Pure: 'class_deps' command visualizes the subclass relation; file | diff | annotate
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary'; file | diff | annotate
2006-09-11 haftmann 2006-09-11 hid succ, pred in Numeral.thy file | diff | annotate
2006-09-06 haftmann 2006-09-06 got rid of Numeral.bin type file | diff | annotate
2006-09-01 haftmann 2006-09-01 final syntax for some Isar code generator keywords file | diff | annotate
2006-08-14 chaieb 2006-08-14 *** empty log message *** file | diff | annotate
2006-08-09 wenzelm 2006-08-09 * ProofContext.prems_limit is now -1 by default; file | diff | annotate
2006-08-08 haftmann 2006-08-08 abandoned equal_list in favor for eq_list file | diff | annotate
2006-08-03 chaieb 2006-08-03 *** empty log message *** file | diff | annotate
2006-08-03 ballarin 2006-08-03 Restructured algebra library, added ideals and quotient rings. file | diff | annotate
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs) file | diff | annotate
2006-07-25 haftmann 2006-07-25 added notes on class_package.ML and codegen_package.ML file | diff | annotate
2006-07-19 ballarin 2006-07-19 Change to algebra method. file | diff | annotate
2006-07-17 webertj 2006-07-17 support for MiniSat proof traces added file | diff | annotate
2006-07-12 wenzelm 2006-07-12 * Isar: ":" (colon) is no longer a symbolic identifier character; file | diff | annotate
2006-07-11 wenzelm 2006-07-11 * Pure: structure Name; file | diff | annotate
2006-07-11 kleing 2006-07-11 hex and binary numerals (contributed by Rafal Kolanski) file | diff | annotate
2006-07-08 wenzelm 2006-07-08 * Pure: structure Variable provides operations for proper treatment of fixed/schematic variables; * Pure: Goal.prove, Goal.prove_global; tuned; file | diff | annotate
2006-07-04 wenzelm 2006-07-04 Isar: 'print_facts' prints all local facts; file | diff | annotate
2006-07-04 ballarin 2006-07-04 Method intro_locales replaced by intro_locales and unfold_locales. file | diff | annotate
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales. file | diff | annotate
2006-06-15 nipkow 2006-06-15 *** empty log message *** file | diff | annotate
2006-06-12 berghofe 2006-06-12 Added "evaluation" method. file | diff | annotate
2006-06-07 wenzelm 2006-06-07 * Theory syntax: some popular names (e.g. "class", "if") are now keywords. * Isar: schematic goals are no longer restricted to higher-order patterns. * ML/Pure: Logic.(un)varify only works in a global context, which is now enforced. file | diff | annotate
2006-06-06 ballarin 2006-06-06 Improved parameter management of locales. file | diff | annotate
2006-05-24 wenzelm 2006-05-24 tuned; file | diff | annotate
2006-05-24 wenzelm 2006-05-24 tuned; file | diff | annotate
2006-05-24 wenzelm 2006-05-24 Pure: update on overloaded defs; file | diff | annotate
2006-05-17 wenzelm 2006-05-17 * Pure: syntax 'CONST name' produces a fully internalized constant; tuned; file | diff | annotate
2006-05-16 wenzelm 2006-05-16 * Isar/locale: 'const_syntax'; file | diff | annotate
2006-05-16 wenzelm 2006-05-16 * Pure/library: divide_and_conquer; * Theory Real: new method ferrack; file | diff | annotate
2006-05-13 wenzelm 2006-05-13 * Pure: overloaded definitions are now actually checked for acyclic dependencies; file | diff | annotate
2006-05-07 wenzelm 2006-05-07 * Isar: removed obsolete 'concl is' patterns. file | diff | annotate
2006-05-05 wenzelm 2006-05-05 * Library: theory Accessible_Part has been move to main HOL. file | diff | annotate
2006-04-30 wenzelm 2006-04-30 * Pure: axclasses now purely definitional; * Pure/kernel: consts certification ignores sort constraints; file | diff | annotate
2006-04-09 nipkow 2006-04-09 *** empty log message *** file | diff | annotate
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation'; file | diff | annotate
2006-03-17 ballarin 2006-03-17 Renamed setsum_mult to setsum_right_distrib. file | diff | annotate
2006-03-17 haftmann 2006-03-17 renamed op < <= to Orderings.less(_eq) file | diff | annotate
2006-03-14 wenzelm 2006-03-14 print_statement; file | diff | annotate
2006-03-14 wenzelm 2006-03-14 Pure: no_translations; file | diff | annotate
2006-03-13 schirmer 2006-03-13 entry for Library/AssocList file | diff | annotate
2006-03-10 wenzelm 2006-03-10 tuned; file | diff | annotate
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc. file | diff | annotate
2006-03-08 wenzelm 2006-03-08 tuned; file | diff | annotate
2006-03-08 wenzelm 2006-03-08 Isar/method: goal restriction; file | diff | annotate
2006-03-08 nipkow 2006-03-08 *** empty log message *** file | diff | annotate
2006-02-16 wenzelm 2006-02-16 tuned; file | diff | annotate
2006-02-16 wenzelm 2006-02-16 tuned; file | diff | annotate
2006-02-16 wenzelm 2006-02-16 tuned; file | diff | annotate
2006-02-16 wenzelm 2006-02-16 * Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization'; file | diff | annotate
2006-02-12 wenzelm 2006-02-12 * ML/Pure/General: improved join interface for tables; file | diff | annotate
2006-02-12 wenzelm 2006-02-12 tuned; file | diff | annotate
2006-02-10 wenzelm 2006-02-10 * ML/Pure: generic Args/Attrib syntax everywhere; file | diff | annotate
2006-02-08 nipkow 2006-02-08 *** empty log message *** file | diff | annotate
2006-02-02 wenzelm 2006-02-02 tuned; file | diff | annotate
2006-02-02 wenzelm 2006-02-02 * Isar: 'obtains' element; file | diff | annotate
2006-01-31 wenzelm 2006-01-31 * Pure: 'advanced' translation functions use Context.generic instead of just theory; file | diff | annotate
isabelle