2007-12-03 haftmann 2007-12-03 interface for unchecked definitions
2007-12-03 haftmann 2007-12-03 shifted "fun" command to Wellfounded_Relations
2007-12-03 haftmann 2007-12-03 updated
2007-12-02 chaieb 2007-12-02 Eliminated unused theorems minusinf_ex and minusinf_bex
2007-11-30 haftmann 2007-11-30 first working version of instance target
2007-11-30 haftmann 2007-11-30 interpretation for typedefs
2007-11-30 haftmann 2007-11-30 using intro_locales instead of unfold_locales if appropriate
2007-11-30 haftmann 2007-11-30 more canonical attribute application
2007-11-30 haftmann 2007-11-30 adjustions to due to instance target
2007-11-30 krauss 2007-11-30 new declaration [[measure_function f]] to tell lexicographic_order about custom measure functions to use.
2007-11-30 nipkow 2007-11-30 *** empty log message ***
2007-11-30 nipkow 2007-11-30 added {#.,.,...#}
2007-11-29 haftmann 2007-11-29 tuned
2007-11-29 haftmann 2007-11-29 stripped down
2007-11-29 wenzelm 2007-11-29 isabelle-process: option -p echos ISABELLE_PID;
2007-11-29 wenzelm 2007-11-29 commit: non-critical, otherwise session restart will result in deadlock!
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-11-29 haftmann 2007-11-29 dropped dead code
2007-11-28 wenzelm 2007-11-28 polyml: default heap size is back to -H 200 (people are still using machines with < 1GB of memory; no need to workaround heap problems of polyml-5.0 anymore);
2007-11-28 urbanc 2007-11-28 an example file for how to treat Felleisen-Hieb-style contexts in nominal
2007-11-28 wenzelm 2007-11-28 removed (cf. object_logic.ML);
2007-11-28 wenzelm 2007-11-28 added base_sort; added typedecl, dependent on base_sort (cf. intermediate typedecl.ML and former sign.ML, HOL/Tools/typedef_package.ML); typedecl: recovered proper use of Syntax.type_name;
2007-11-28 wenzelm 2007-11-28 removed typedecl.ML (cf. object_logic.ML);
2007-11-28 wenzelm 2007-11-28 ObjectLogic.typedecl;
2007-11-28 wenzelm 2007-11-28 replaced typedecl interpretation by ObjectLogic.typedecl (based on base_sort);
2007-11-28 paulson 2007-11-28 simplified using sledgehammer
2007-11-28 paulson 2007-11-28 Chained theorems are no longer mentioned in metis calls and (if used) they prevent the output of a structured proof.
2007-11-28 paulson 2007-11-28 comment
2007-11-28 haftmann 2007-11-28 (reverted to unnamed infix)
2007-11-28 haftmann 2007-11-28 simplified interpretations
2007-11-28 haftmann 2007-11-28 deleted looping code theorem
2007-11-28 berghofe 2007-11-28 to_set now applies collect_mem_simproc as well.
2007-11-28 haftmann 2007-11-28 naming policy for instances
2007-11-28 haftmann 2007-11-28 tuned interfaces of class module
2007-11-28 haftmann 2007-11-28 dropped dead code
2007-11-28 haftmann 2007-11-28 dropped legacy unnamed infix
2007-11-28 haftmann 2007-11-28 dropped implicit assumption proof
2007-11-28 haftmann 2007-11-28 dropped legacy ml bindings
2007-11-27 wenzelm 2007-11-27 tuned titles;
2007-11-27 wenzelm 2007-11-27 moved titles;
2007-11-27 wenzelm 2007-11-27 tuned title;
2007-11-27 wenzelm 2007-11-27 tuned titles;
2007-11-27 wenzelm 2007-11-27 standard_parse_term: check ambiguous results without changing the result yet;
2007-11-27 wenzelm 2007-11-27 challenge by John Harrison: down to 12s (was 17s, was 75s);
2007-11-27 wenzelm 2007-11-27 Knaster_Tarski: turned into Isar statement, tuned proofs;
2007-11-27 berghofe 2007-11-27 first_order_match now only calls loose_bvar when inside an abstraction.
2007-11-27 berghofe 2007-11-27 check_conv now only performs beta-eta-normalization when equations cannot be combined just by transitivity.
2007-11-27 berghofe 2007-11-27 Optimized beta_norm: only tries to normalize term when it contains abstractions.
2007-11-27 berghofe 2007-11-27 Better error messages for cterm_instantiate.
2007-11-26 wenzelm 2007-11-26 some more lemmas due to Peter Lammich;
2007-11-26 wenzelm 2007-11-26 Peter Lammich: HOL-Lattice lemmas;
2007-11-26 nipkow 2007-11-26 Removed forced roman font in mode=IfThen.
2007-11-26 wenzelm 2007-11-26 use official polyml-5.1;
2007-11-26 wenzelm 2007-11-26 tuned comments; tuned;
2007-11-26 wenzelm 2007-11-26 moved new NEWS from Isabelle2007 to this Isabelle version'';
2007-11-26 haftmann 2007-11-26 simplified website rsync
2007-11-23 haftmann 2007-11-23 rudimentary instantiation target
2007-11-23 haftmann 2007-11-23 explicit type signature
2007-11-23 haftmann 2007-11-23 interpretation of typedecls: instantiation to class type
2007-11-23 haftmann 2007-11-23 deleted card definition as code lemma; authentic syntax for card