2008-08-06 ballarin 2008-08-06 Interpretation command (theory/proof context) no longer simplifies goal.
2008-08-06 nipkow 2008-08-06 added lemma
2008-08-06 wenzelm 2008-08-06 made SML/NJ happy;
2008-08-06 berghofe 2008-08-06 Reverted last change, since it caused incompatibilities.
2008-08-06 wenzelm 2008-08-06 fall back on P.term_group, to avoid problems with inner_syntax markup (due to CodeName.read_const_exprs);
2008-08-06 wenzelm 2008-08-06 T.end_position_of; tuned;
2008-08-06 wenzelm 2008-08-06 adapted Antiq;
2008-08-06 wenzelm 2008-08-06 parse_sort/typ/term/prop: report markup;
2008-08-06 wenzelm 2008-08-06 sort/typ/term/prop: inner_syntax markup encodes original source position; added typ/term/prop_group (without inner_syntax markup);
2008-08-06 wenzelm 2008-08-06 removed obsolete range_of (already included in position); added end_position_of; replaced scan_string by scan_quoted (which keeps quotes and includes alt_string as well); misc tuning;
2008-08-06 wenzelm 2008-08-06 report markup;
2008-08-06 wenzelm 2008-08-06 Antiq: inner vs. outer position; scan_antiq: use T.scan_quoted;
2008-08-06 wenzelm 2008-08-06 of_properties: observe Markup.position_properties';
2008-08-06 wenzelm 2008-08-06 added position_properties'; renamed prop to proposition; added attribute, method;
2008-08-05 wenzelm 2008-08-05 token: maintain of source, which retains original position information; removed count/counted, advance position via scanned source;
2008-08-05 wenzelm 2008-08-05 moved OuterLex.count here;
2008-08-05 wenzelm 2008-08-05 improved recover: also resync on symbol/comment/verbatim delimiters;
2008-08-05 wenzelm 2008-08-05 advance: operate on symbol list (less overhead);
2008-08-05 wenzelm 2008-08-05 added token;
2008-08-05 krauss 2008-08-05 fix HOL/ex/LexOrds.thy; add to regression
2008-08-05 wenzelm 2008-08-05 added report;
2008-08-05 wenzelm 2008-08-05 removed axiom; added fact, dynamic_fact, prop;
2008-08-05 wenzelm 2008-08-05 get_fact: report position;
2008-08-05 wenzelm 2008-08-05 Facts.lookup: return static/dynamic status;
2008-08-04 wenzelm 2008-08-04 position scanner: encode token range;
2008-08-04 wenzelm 2008-08-04 added encode_range; tuned;
2008-08-04 wenzelm 2008-08-04 added end_line, end_column properties;
2008-08-04 wenzelm 2008-08-04 meta_subst: xsymbols make it work with clean Pure;
2008-08-04 wenzelm 2008-08-04 abstract type Scan.stopper, position taken from last input token;
2008-08-04 wenzelm 2008-08-04 abstract type Scan.stopper;
2008-08-04 wenzelm 2008-08-04 abstract type stopper, may depend on final input;
2008-08-04 wenzelm 2008-08-04 removed obsolete apply_theorems(_i);
2008-08-04 wenzelm 2008-08-04 tuned signature; eliminated obsolete pervasives;
2008-08-04 wenzelm 2008-08-04 removed obsolete note_thms_cmd;
2008-08-04 wenzelm 2008-08-04 simplified defer_recdef(_i): plain facts via Attrib.eval_thms;
2008-08-04 wenzelm 2008-08-04 tuned description;
2008-08-04 wenzelm 2008-08-04 replaced mercurial.cgi by hgwebdir.cgi, resulting in http://isabelle.in.tum.de/repos/isabelle/
2008-08-04 berghofe 2008-08-04 Quoted terms in consts_code declarations are now preprocessed as well.
2008-08-04 berghofe 2008-08-04 Exported eval_wrapper.
2008-08-04 berghofe 2008-08-04 - corrected bogus comment for function inst_conj_all - tuned function obtain_fresh_name
2008-08-04 krauss 2008-08-04 removed dead code
2008-08-04 wenzelm 2008-08-04 simplified prepare_command;
2008-08-04 wenzelm 2008-08-04 Isar.command: explicitly set transaction position, as required for prepare_command errors; adapted Isabelle.command;
2008-08-04 ballarin 2008-08-04 Updated locale tests.
2008-08-01 ballarin 2008-08-01 Generalised polynomial lemmas from cring to ring.
2008-08-01 ballarin 2008-08-01 Removed import and lparams from locale record.
2008-08-01 nipkow 2008-08-01 made setsum executable on int.
2008-07-31 ballarin 2008-07-31 Tuned (for the sake of a meaningless log entry).
2008-07-30 ballarin 2008-07-30 New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-07-30 nipkow 2008-07-30 added hint about writing "x : set xs".
2008-07-30 haftmann 2008-07-30 simple lifters
2008-07-30 haftmann 2008-07-30 dropped imperative monad bind
2008-07-30 haftmann 2008-07-30 facts_of
2008-07-30 haftmann 2008-07-30 improved morphism
2008-07-30 haftmann 2008-07-30 SML_imp, OCaml_imp
2008-07-30 haftmann 2008-07-30 clarified
2008-07-30 haftmann 2008-07-30 tuned
2008-07-29 ballarin 2008-07-29 Zorn's Lemma for partial orders.
2008-07-29 ballarin 2008-07-29 Definitions and some lemmas for reflexive orderings.
2008-07-29 ballarin 2008-07-29 Lemmas added