isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -112 +112 +1000 +3000 +10000 +30000 tip

Renamed inductive2 to inductive.
2007-07-11, by berghofe
acc is now defined using inductive_set.
2007-07-11, by berghofe
Added new package for inductive sets.
2007-07-11, by berghofe
Adapted to new inductive definition package.
2007-07-11, by berghofe
Adapted to changes in inductive definition package.
2007-07-11, by berghofe
tuned comment markup;
2007-07-11, by wenzelm
treat OuterLex.Error;
2007-07-11, by wenzelm
separated Malformed (symbolic char) from Error (bad input);
2007-07-11, by wenzelm
Output.escape_malformed;
2007-07-11, by wenzelm
added escape_malformed (failsafe);
2007-07-11, by wenzelm
Basic editing of theory sources.
2007-07-10, by wenzelm
tuned;
2007-07-10, by wenzelm
export html_mode, begin_document, end_document;
2007-07-10, by wenzelm
renamed XML.Rawtext to XML.Output;
2007-07-10, by wenzelm
export get_lexicons;
2007-07-10, by wenzelm
added kind_of;
2007-07-10, by wenzelm
Markup.enclose;
2007-07-10, by wenzelm
more markup for inner and outer syntax;
2007-07-10, by wenzelm
simplified funpow, untabify;
2007-07-10, by wenzelm
added Thy/thy_edit.ML;
2007-07-10, by wenzelm
added some markup for outer syntax;
2007-07-10, by wenzelm
clarified merge of module names
2007-07-10, by haftmann
now a monolithic module
2007-07-10, by haftmann
now works with SML/NJ
2007-07-10, by haftmann
tuned
2007-07-10, by haftmann
improvement for code names
2007-07-10, by haftmann
removed proof dependency on transitivity theorems
2007-07-10, by haftmann
moved lfp_induct2 here
2007-07-10, by haftmann
clarified import
2007-07-10, by haftmann
moved lfp_induct2 to Relation.thy
2007-07-10, by haftmann
moved some finite lemmas here
2007-07-10, by haftmann
moved finite lemmas to Finite_Set.thy
2007-07-10, by haftmann
added print_mode setup (from pretty.ML);
2007-07-10, by wenzelm
Markup.add_mode;
2007-07-10, by wenzelm
removed no_state markup -- produce empty state;
2007-07-10, by wenzelm
Markup.output;
2007-07-10, by wenzelm
moved source cascading from scan.ML to source.ML;
2007-07-10, by wenzelm
infixr || (more efficient);
2007-07-10, by wenzelm
moved print_mode setup for markup to markup.ML;
2007-07-10, by wenzelm
Markup.output;
2007-07-10, by wenzelm
use position.ML earlier;
2007-07-10, by wenzelm
Add widthN to signature
2007-07-10, by aspinall
cd ISABELLE_HOME/etc;
2007-07-10, by wenzelm
adjusted
2007-07-10, by haftmann
updated keywords
2007-07-10, by haftmann
simplified, tuned
2007-07-10, by haftmann
re-expanded paths
2007-07-10, by haftmann
replaced code generator framework for reflected cooper
2007-07-10, by haftmann
expanded fragile proof
2007-07-10, by haftmann
extended - convers now basic lcm properties also
2007-07-10, by haftmann
constant dvd now in class target
2007-07-10, by haftmann
moved lemma zdvd_period here
2007-07-10, by haftmann
introduced (auxiliary) class dvd_mod for more convenient code generation
2007-07-10, by haftmann
tuned;
2007-07-10, by wenzelm
nested source: explicit interactive flag for recover avoids duplicate errors;
2007-07-10, by wenzelm
tuned dead code;
2007-07-09, by wenzelm
use Position.file_of;
2007-07-09, by wenzelm
toplevel_source: interactive flag indicates intermittent error_msg;
2007-07-09, by wenzelm
Malformed token: error msg;
2007-07-09, by wenzelm
adapted OuterLex/T.source;
2007-07-09, by wenzelm
scan: changed treatment of malformed symbols, passed to next stage;
2007-07-09, by wenzelm
nested source: error msg passed to recover;
2007-07-09, by wenzelm
tuned signature;
2007-07-09, by wenzelm
replaced name by file (unquoted);
2007-07-09, by wenzelm
moved Path.position to Position.path;
2007-07-09, by wenzelm
proper position markup;
2007-07-09, by wenzelm
use position.ML after pretty.ML;
2007-07-09, by wenzelm
removed target RAW-ProofGeneral (impractical to maintain);
2007-07-09, by wenzelm
declare: disallow quote (") in names;
2007-07-09, by wenzelm
removed legacy ML file;
2007-07-09, by wenzelm
HOL-Complex-Matrix: fixed deps -- sort of;
2007-07-09, by wenzelm
adopted to new computing oracle and fixed bugs introduced by tuning
2007-07-09, by obua
added computing oracle support for HOL and numerals
2007-07-09, by obua
new version of computing oracle
2007-07-09, by obua
simplified writeln_fn;
2007-07-09, by wenzelm
prompt: plain string, not output;
2007-07-09, by wenzelm
type output = string indicates raw system output;
2007-07-09, by wenzelm
symbolic output: avoid empty blocks, 1 space for fbreak;
2007-07-08, by wenzelm
tuned;
2007-07-08, by wenzelm
thm tag: Markup.property list;
2007-07-08, by wenzelm
gensym: slightly more obscure prefix descreases probability of name clash;
2007-07-08, by wenzelm
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-07-08, by wenzelm
attribute tagged: single argument;
2007-07-08, by wenzelm
updated;
2007-07-08, by wenzelm
simplified Symtab;
2007-07-08, by wenzelm
renamed ML_exc to ML_exn;
2007-07-08, by wenzelm
Show the use of reflection attribute; fixed comments about the order of absorbing equations : f (C x) = x ; now automaically tried as last;
2007-07-08, by chaieb
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
2007-07-08, by chaieb
Try several correctness theorems for reflection; rearrange cong rules to avoid the absoption cases;
2007-07-08, by chaieb
Context data now consist of eqations for reification and equations for correctness theorems for reflection; Added attribute reflection to store correctness theorems to be trued by default
2007-07-08, by chaieb
simplified/more robust print_state;
2007-07-08, by wenzelm
export mode_markup;
2007-07-08, by wenzelm
added markup for pretty printing;
2007-07-08, by wenzelm
Corrected erronus use of compiletime context to the runtime context
2007-07-08, by chaieb
make smlnj happy;
2007-07-07, by wenzelm
toplevel prompt/print_state: proper markup, removed hooks;
2007-07-07, by wenzelm
toplevel prompt/print_state: proper markup, removed hooks;
2007-07-07, by wenzelm
pretty_state: subgoal markup;
2007-07-07, by wenzelm
added markup_chunks;
2007-07-07, by wenzelm
added toplevel markup;
2007-07-07, by wenzelm
use markup.ML earlier;
2007-07-07, by wenzelm
removed obsolete disable_pr/enable_pr;
2007-07-07, by wenzelm
pretty_goals_aux: subgoal markup;
2007-07-07, by wenzelm
pr_goals: adapted Display.pretty_goals_aux;
2007-07-07, by wenzelm
export attribute;
2007-07-07, by wenzelm
pretty_sort/typ/term: markup;
2007-07-07, by wenzelm
pretty: markup for syntax/name of authentic consts;
2007-07-07, by wenzelm
depend on alist.ML, markup.ML;
2007-07-07, by wenzelm
markup: emit as control information -- no indent text;
2007-07-07, by wenzelm
added property conversions;
2007-07-07, by wenzelm
position: line and name;
2007-07-07, by wenzelm
moved markup.ML before position.ML;
2007-07-07, by wenzelm