isabelle: Graph

refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
2008-08-15, by wenzelm
refined JVM path wrappers;
2008-08-15, by wenzelm
added JVM components (Scala or Java);
2008-08-15, by wenzelm
tuned;
2008-08-15, by wenzelm
jars: build Pure.jar;
2008-08-15, by wenzelm
scan: proper recovery for escaped \\< symbols;
2008-08-15, by wenzelm
basic setup for Scala material;
2008-08-15, by wenzelm
Basic support for Isabelle symbols.
2008-08-15, by wenzelm
added some abbrevs;
2008-08-15, by wenzelm
removed redundant "symbol" property;
2008-08-15, by wenzelm
Default interpretation of some Isabelle symbols.
2008-08-15, by wenzelm
report antiquotation names;
2008-08-15, by wenzelm
fixed DOCTYPE -- XHTML is case-sensitive!
2008-08-15, by wenzelm
report antiquotation names;
2008-08-15, by wenzelm
added ML_antiq, doc_antiq;
2008-08-15, by wenzelm
added README;
2008-08-15, by wenzelm
generated truetype font;
2008-08-15, by wenzelm
The Jerusalem font from 2004 -- unicode version.
2008-08-15, by wenzelm
args: explicit groups for file_name, theory_name;
2008-08-15, by wenzelm
read_asts: Lexicon.report_token, filter Lexicon.is_proper;
2008-08-15, by wenzelm
filter Lexicon.is_proper -- Lexicon.tokenize now includes improper tokens;
2008-08-15, by wenzelm
token_kind: add Space, Comment;
2008-08-15, by wenzelm
renamed T.source_of' to T.source_position_of;
2008-08-15, by wenzelm
renamed T.source_of' to T.source_position_of;
2008-08-15, by wenzelm
output_markup: check Markup.is_none;
2008-08-15, by wenzelm
added is_none;
2008-08-15, by wenzelm
Args.name_source(_position) for proper position information;
2008-08-15, by wenzelm
[source=false] for quoted antiquotation avoids quote-escapes in output;
2008-08-14, by wenzelm
report antiquotations;
2008-08-14, by wenzelm
tuned;
2008-08-14, by wenzelm
report ML_source;
2008-08-14, by wenzelm
renamed P.ml_source to P.ML_source;
2008-08-14, by wenzelm
report doc_source;
2008-08-14, by wenzelm
added ML_source, doc_source;
2008-08-14, by wenzelm
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
2008-08-14, by wenzelm
added source_of';
2008-08-14, by wenzelm
P.doc_source and P.ml_sorce for proper SymbolPos.text;
2008-08-14, by wenzelm
oracle, header/local_theory/proof_markup: pass SymbolPos.text;
2008-08-14, by wenzelm
use SymbolPos.T list directly, instead of encoded SymbolPos.text;
2008-08-14, by wenzelm
ML_Context.add_antiq: pass position;
2008-08-14, by wenzelm
ML_Context.add_antiq: pass position;
2008-08-14, by wenzelm
retrieve_thms: transfer fact position to result;
2008-08-14, by wenzelm
moved basic thm operations from structure PureThy to Thm;
2008-08-14, by wenzelm
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-14, by wenzelm
made SML/NJ happy;
2008-08-14, by wenzelm
removed obsolete present_html -- now part of regular theory presentation;
2008-08-13, by wenzelm
removed obsolete verbatim_source, results, chapter, section etc.;
2008-08-13, by wenzelm
removed obsolete verbatim_source, results, chapter, section etc.;
2008-08-13, by wenzelm
ProofDisplay.add_hook;
2008-08-13, by wenzelm
simplified present_local_theory/proof;
2008-08-13, by wenzelm
ProofDisplay.theory_results;
2008-08-13, by wenzelm
removed obsolete present_results;
2008-08-13, by wenzelm
scan: SymbolPos.tabify_content when creating tokens (for proper presentation output);
2008-08-13, by wenzelm
load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
2008-08-13, by wenzelm
simplified markup commands;
2008-08-13, by wenzelm
simplified markup commands -- removed obsolete Present.results, always check text;
2008-08-13, by wenzelm
added untabify_content;
2008-08-13, by wenzelm
tuned;
2008-08-13, by wenzelm
removed obsolete untabify (superceded by SymbolPos.tabify_content);
2008-08-13, by wenzelm
tuned document;
2008-08-13, by wenzelm
removed obsolete theorems;
2008-08-13, by wenzelm
Changed proof of strong induction rule to avoid infinite loop
2008-08-13, by berghofe
token_kind_markup: complete coverage;
2008-08-12, by wenzelm
OuterSyntax.scan: pass position;
2008-08-12, by wenzelm
message: ignored if body empty;
2008-08-12, by wenzelm
load_thy: removed obsolete dir argument;
2008-08-12, by wenzelm
abstract type span, tuned interfaces;
2008-08-12, by wenzelm
adapted ThyEdit operations;
2008-08-12, by wenzelm
added ignored, malformed transitions;
2008-08-12, by wenzelm
Symbol.source/OuterLex.source: more explicit do_recover argument;
2008-08-12, by wenzelm
Isabelle.command: inline former OuterSyntax.prepare_command;
2008-08-12, by wenzelm
load thy_edit.ML before outer_syntax.ML;
2008-08-12, by wenzelm
renamed unknown_span to malformed_span;
2008-08-12, by wenzelm
Symbol.source/OuterLex.source: more explicit do_recover argument;
2008-08-12, by wenzelm
updated generated file;
2008-08-12, by wenzelm
rudimentary code setup for set operations
2008-08-11, by haftmann
<applet>: more XHTML 1.0 Transitional conformance;
2008-08-11, by wenzelm
Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;
2008-08-11, by wenzelm
<pre>: removed xml:space, is already default;
2008-08-11, by wenzelm
produce XHTML 1.0 Transitional;
2008-08-11, by wenzelm
renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
2008-08-11, by wenzelm
Isar.command: do not set position of enclosing transaction, to avoid of clash with the one being prepared here!
2008-08-11, by wenzelm
changed code setup
2008-08-11, by haftmann
re-arranged class dense_linear_order
2008-08-11, by haftmann
rudimentary code setup for set operations
2008-08-11, by haftmann
moved class wellorder to theory Orderings
2008-08-11, by haftmann
added parse_token (from proof_context.ML);
2008-08-10, by wenzelm
read_tyname/const/const_proper: report position;
2008-08-10, by wenzelm
pass position to get_fact;
2008-08-10, by wenzelm
pass token source to typ/term etc.;
2008-08-10, by wenzelm
added name property operation;
2008-08-10, by wenzelm
renamed ML_Lex.val_of to content_of;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
unified Args.T with OuterLex.token;
2008-08-09, by wenzelm
load args.ML later (after outer_parse.ML);
2008-08-09, by wenzelm
unified Args.T with OuterLex.token, renamed some operations;
2008-08-09, by wenzelm
read_asts: report literal tokens;
2008-08-09, by wenzelm
tuned error message;
2008-08-09, by wenzelm
pos_of_token: Position.T;
2008-08-09, by wenzelm
dest: sort strings;
2008-08-09, by wenzelm
added literal;
2008-08-09, by wenzelm
read_token: more robust handling of empty text;
2008-08-09, by wenzelm
datatype token: maintain range, tuned representation;
2008-08-09, by wenzelm
datatype token: maintain range, tuned representation;
2008-08-09, by wenzelm
datatype token: maintain range, tuned representation;
2008-08-09, by wenzelm
tuned SymbolPos interface;
2008-08-09, by wenzelm
YXML.parse: allow text without markup, potentially empty;
2008-08-09, by wenzelm
added content;
2008-08-09, by wenzelm
added distance_of (permissive version);
2008-08-09, by wenzelm
count offset as well;
2008-08-08, by wenzelm
added offset/end_offset;
2008-08-08, by wenzelm
tuned formatting;
2008-08-08, by wenzelm
clean up dead code
2008-08-08, by krauss
made SML/NJ happy;
2008-08-08, by wenzelm
FundefLib.try_proof : attempt a proof and see if it works
2008-08-08, by krauss
added lemmas
2008-08-08, by nipkow
inner_syntax markup is back;
2008-08-07, by wenzelm
disabled inner_syntax markup for now;
2008-08-07, by wenzelm
added read_token -- with optional YXML encoding of position;
2008-08-07, by wenzelm
parse_token: use Syntax.read_token, pass full position information;
2008-08-07, by wenzelm
tuned;
2008-08-07, by wenzelm
map_default: more explicit scope;
2008-08-07, by wenzelm
datatype lexicon: alternative representation using nested Symtab.table;
2008-08-07, by wenzelm
simplified Antiquote signature;
2008-08-07, by wenzelm
more precise positions due to SymbolsPos.implode_delim;
2008-08-07, by wenzelm
simplified Antiq: regular SymbolPos.text with position;
2008-08-07, by wenzelm
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
2008-08-07, by wenzelm
only increment column if valid;
2008-08-07, by wenzelm
install_pp Position.T;
2008-08-07, by wenzelm
Position.start;
2008-08-07, by wenzelm
SymbolPos.explode;
2008-08-07, by wenzelm
improved position handling due to SymbolPos.T;
2008-08-07, by wenzelm
improved position handling due to SymbolPos.T;
2008-08-07, by wenzelm
Antiquote.read/read_arguments;
2008-08-07, by wenzelm
updated type of nested sources;
2008-08-07, by wenzelm
improved position handling due to SymbolPos.T;
2008-08-07, by wenzelm
adapted Scan.extend_lexicon/merge_lexicons;
2008-08-07, by wenzelm
renamed scan_antiquotes to read;
2008-08-07, by wenzelm
export not_eof;
2008-08-07, by wenzelm
reorganized lexicon: allow scanning of annotated symbols, tuned representation and interfaces;
2008-08-07, by wenzelm
advance: single argument (again);
2008-08-07, by wenzelm
Symbols with explicit position information.
2008-08-07, by wenzelm
added General/symbol_pos.ML;
2008-08-07, by wenzelm
Interpretation command (theory/proof context) no longer simplifies goal.
2008-08-06, by ballarin
added lemma
2008-08-06, by nipkow
made SML/NJ happy;
2008-08-06, by wenzelm
Reverted last change, since it caused incompatibilities.
2008-08-06, by berghofe
fall back on P.term_group, to avoid problems with inner_syntax markup (due to CodeName.read_const_exprs);
2008-08-06, by wenzelm
T.end_position_of;
2008-08-06, by wenzelm
adapted Antiq;
2008-08-06, by wenzelm
parse_sort/typ/term/prop: report markup;
2008-08-06, by wenzelm
sort/typ/term/prop: inner_syntax markup encodes original source position;
2008-08-06, by wenzelm
removed obsolete range_of (already included in position);
2008-08-06, by wenzelm
report markup;
2008-08-06, by wenzelm
Antiq: inner vs. outer position;
2008-08-06, by wenzelm
of_properties: observe Markup.position_properties';
2008-08-06, by wenzelm
added position_properties';
2008-08-06, by wenzelm
token: maintain of source, which retains original position information;
2008-08-05, by wenzelm
moved OuterLex.count here;
2008-08-05, by wenzelm
improved recover: also resync on symbol/comment/verbatim delimiters;
2008-08-05, by wenzelm
advance: operate on symbol list (less overhead);
2008-08-05, by wenzelm
added token;
2008-08-05, by wenzelm
fix HOL/ex/LexOrds.thy; add to regression
2008-08-05, by krauss
added report;
2008-08-05, by wenzelm
removed axiom;
2008-08-05, by wenzelm
get_fact: report position;
2008-08-05, by wenzelm
Facts.lookup: return static/dynamic status;
2008-08-05, by wenzelm
position scanner: encode token range;
2008-08-04, by wenzelm
added encode_range;
2008-08-04, by wenzelm
added end_line, end_column properties;
2008-08-04, by wenzelm
meta_subst: xsymbols make it work with clean Pure;
2008-08-04, by wenzelm
abstract type Scan.stopper, position taken from last input token;
2008-08-04, by wenzelm
abstract type Scan.stopper;
2008-08-04, by wenzelm
abstract type stopper, may depend on final input;
2008-08-04, by wenzelm
removed obsolete apply_theorems(_i);
2008-08-04, by wenzelm
tuned signature;
2008-08-04, by wenzelm
removed obsolete note_thms_cmd;
2008-08-04, by wenzelm
simplified defer_recdef(_i): plain facts via Attrib.eval_thms;
2008-08-04, by wenzelm
tuned description;
2008-08-04, by wenzelm
replaced mercurial.cgi by hgwebdir.cgi, resulting in http://isabelle.in.tum.de/repos/isabelle/
2008-08-04, by wenzelm
Quoted terms in consts_code declarations are now preprocessed as well.
2008-08-04, by berghofe
Exported eval_wrapper.
2008-08-04, by berghofe
- corrected bogus comment for function inst_conj_all
2008-08-04, by berghofe
removed dead code
2008-08-04, by krauss
simplified prepare_command;
2008-08-04, by wenzelm
Isar.command: explicitly set transaction position, as required for prepare_command errors;
2008-08-04, by wenzelm
Updated locale tests.
2008-08-04, by ballarin
Generalised polynomial lemmas from cring to ring.
2008-08-01, by ballarin
Removed import and lparams from locale record.
2008-08-01, by ballarin
made setsum executable on int.
2008-08-01, by nipkow
Tuned (for the sake of a meaningless log entry).
2008-07-31, by ballarin
New locales for orders and lattices where the equivalence relation is not restricted to equality.
2008-07-30, by ballarin
added hint about writing "x : set xs".
2008-07-30, by nipkow
simple lifters
2008-07-30, by haftmann
dropped imperative monad bind
2008-07-30, by haftmann
facts_of
2008-07-30, by haftmann
improved morphism
2008-07-30, by haftmann
SML_imp, OCaml_imp
2008-07-30, by haftmann
clarified
2008-07-30, by haftmann
tuned
2008-07-30, by haftmann
Zorn's Lemma for partial orders.
2008-07-29, by ballarin
Definitions and some lemmas for reflexive orderings.
2008-07-29, by ballarin
Lemmas added
2008-07-29, by ballarin
New theory on divisibility.
2008-07-29, by ballarin
Renamed theorems;
2008-07-29, by ballarin
New theorems on summation.
2008-07-29, by ballarin
Unit_inv_l, Unit_inv_r made [simp].
2008-07-29, by ballarin
New theory on divisibility;
2008-07-29, by ballarin
Unit_inv_l, Unit_inv_r made [simp];
2008-07-29, by ballarin
Haskell now living in the RealWorld
2008-07-29, by haftmann
corrected Pure dependency
2008-07-29, by haftmann
added removeAll
2008-07-29, by nipkow
tuned; explicit export of element accessors
2008-07-29, by haftmann
PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-07-29, by haftmann
some steps towards explicit class target for canonical interpretation
2008-07-29, by haftmann
declare
2008-07-29, by haftmann
*** empty log message ***
2008-07-28, by nipkow
simplified a proof
2008-07-27, by urbanc
tuned function name
2008-07-26, by haftmann
tuned bootstrap order
2008-07-26, by haftmann
subclass now also works for subclasses with empty specificaton
2008-07-25, by haftmann
dropped PureThy.note; added PureThy.add_thm
2008-07-25, by haftmann
added class preorder
2008-07-25, by haftmann
dropped locale (open)
2008-07-25, by haftmann
added explicit root theory; some tuning
2008-07-25, by haftmann
tuned
2008-07-25, by haftmann
dropped locale (open)
2008-07-25, by haftmann
(re-)added simp rules for (_ + _) div/mod _
2008-07-21, by haftmann
(re-)added simp rules for (_ + _) div/mod _
2008-07-21, by haftmann
added explicit purge_data
2008-07-21, by haftmann
added code generation
2008-07-21, by haftmann
fixed code generator setup
2008-07-21, by haftmann
(adjusted)
2008-07-21, by haftmann
Tuned and corrected ideal_tac for algebra.
2008-07-21, by chaieb
Theorems divides_le, ind_euclid, bezout_lemma, bezout_add, bezout, bezout_add_strong, gcd_unique,gcd_eq, bezout_gcd, bezout_gcd_strong, gcd_mult_distrib, gcd_bezout to GCD.thy
2008-07-21, by chaieb
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
2008-07-21, by chaieb