isabelle: Graph

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

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
The order for parameter for interpretation is now inversted:
2007-07-07, by chaieb
Common markup elements.
2007-07-07, by wenzelm
simplified pretty token metric: type int;
2007-07-07, by wenzelm
simplified pretty token metric: type int;
2007-07-07, by wenzelm
moved General/xml.ML to Tools/xml.ML;
2007-07-07, by wenzelm
tuned;
2007-07-07, by wenzelm
simplified output mode setup;
2007-07-07, by wenzelm
added print_mode setup: indent and markup;
2007-07-07, by wenzelm
renamed raw to escape;
2007-07-07, by wenzelm
simplified pretty token metric: type int;
2007-07-07, by wenzelm
moved General/xml.ML to Tools/xml.ML;
2007-07-07, by wenzelm
added General/markup.ML;
2007-07-07, by wenzelm
added class skolem, command;
2007-07-07, by wenzelm
more interpretations
2007-07-06, by nipkow
Produce good PGML 2.0
2007-07-06, by aspinall
cosmetic (line length fixed)
2007-07-06, by webertj
Some examples for reifying type variables
2007-07-06, by chaieb
Tuned document
2007-07-06, by chaieb
Cleaned add and del attributes
2007-07-06, by chaieb
Reification now deals with type variables
2007-07-06, by chaieb
Cumulative reports for Poly/ML profiling output.
2007-07-06, by wenzelm
Update PGML version, add system name
2007-07-05, by aspinall
tuned interfaces: atomize, atomize_prems, atomize_prems_tac;
2007-07-05, by wenzelm
added type conv;
2007-07-05, by wenzelm
removed comments -- no exception TERM;
2007-07-05, by wenzelm
added is_reflexive;
2007-07-05, by wenzelm
tuned;
2007-07-05, by wenzelm
simplified has_meta_prems;
2007-07-05, by wenzelm
moved type conv to thm.ML;
2007-07-05, by wenzelm
the_theory/proof: error instead of exception Fail;
2007-07-05, by wenzelm
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-05, by wenzelm
renamed Conv.is_refl to Thm.is_reflexive;
2007-07-05, by wenzelm
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-05, by wenzelm
simplified ObjectLogic.atomize;
2007-07-05, by wenzelm
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-05, by wenzelm
Revert body of pgml to match schema for now [change bad for Broker]
2007-07-05, by aspinall
Classify -- comments as ordinary comments (no undo)
2007-07-05, by aspinall
tuned;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
sort_le: tuned eq case;
2007-07-05, by wenzelm
tuned goal conversion interfaces;
2007-07-05, by wenzelm
else_conv: only handle THM | CTERM | TERM | TYPE;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
tuned;
2007-07-05, by wenzelm
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
avoid polymorphic equality;
2007-07-05, by wenzelm
removed dest_cTrueprop (cf. ObjectLogic.dest_judgment);
2007-07-05, by wenzelm
Logical operations on numerals (see also HOL/hologic.ML).
2007-07-05, by wenzelm
added Tools/numeral.ML;
2007-07-05, by wenzelm
common normalizer_funs, avoid cterm_of;
2007-07-05, by wenzelm
Numeral.mk_cnumber;
2007-07-05, by wenzelm