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

Added new program extraction examples.
2007-11-13, by berghofe
New case studies for program extraction.
2007-11-13, by berghofe
Moved auxiliary lemmas to separate theory.
2007-11-13, by berghofe
Added new exampes Greatest_Common_Divisor and Euclid.
2007-11-13, by berghofe
Moved nat_eq_dec to Util.thy
2007-11-13, by berghofe
Moved nat_eq_dec and search to Util.thy
2007-11-13, by berghofe
Tuned.
2007-11-13, by berghofe
to_pred and to_set now save induction and case rule tags.
2007-11-13, by berghofe
removed left-over text links from lynx conversion;
2007-11-12, by wenzelm
back to sigusr2, after Poly/ML 5.1 has been adapted;
2007-11-12, by wenzelm
changed Posix.Signal.usr2 to Posix.Signal.usr1 to make it work with Poly/ML 5.1;
2007-11-12, by wenzelm
updates
2007-11-12, by nipkow
updated
2007-11-12, by haftmann
reactivated default paragraph formatting for ``proof documents'';
2007-11-12, by wenzelm
fixed typo;
2007-11-12, by schirmer
added signatures;
2007-11-12, by schirmer
abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
2007-11-11, by wenzelm
simplified Consts.dest;
2007-11-11, by wenzelm
simplified Consts.dest;
2007-11-11, by wenzelm
simplified Consts.dest;
2007-11-11, by wenzelm
updates
2007-11-11, by nipkow
avoid ML print in production code;
2007-11-11, by wenzelm
updated;
2007-11-11, by wenzelm
auto quickcheck: reduced messages;
2007-11-11, by wenzelm
notation works with any known constant (including fixes/abbrevs);
2007-11-11, by wenzelm
HOL-Statespace;
2007-11-11, by wenzelm
* HOL-Statespace;
2007-11-11, by wenzelm
restore interrupt handler on init;
2007-11-11, by wenzelm
abbrev: back to PrintMode.internal, which works at least half-way;
2007-11-11, by wenzelm
syntax operations: turned extend'' into update'' (absorb duplicates);
2007-11-11, by wenzelm
replaced extend_prtabs by update_prtabs (absorb duplicates);
2007-11-11, by wenzelm
abbrev: PrintMode.input instead of PrintMode.internal for global version!
2007-11-11, by wenzelm
renamed update_list to cons_list;
2007-11-11, by wenzelm
syntax operations: turned extend'' into update'' (absorb duplicates);
2007-11-11, by wenzelm
renamed Symtab.update_list to Symtab.cons_list;
2007-11-11, by wenzelm
tuned specifications of 'notation';
2007-11-11, by wenzelm
added update_const_gram (avoids duplicates);
2007-11-10, by wenzelm
remove_prtabs: tuned, avoid excessive garbage;
2007-11-10, by wenzelm
update_modesyntax: based on Syntax.update_const_gram (avoids duplicates);
2007-11-10, by wenzelm
similar_types: uniform treatment of TFrees/TVars;
2007-11-10, by wenzelm
notation: based on Syntax.update_const_gram (avoids duplicates);
2007-11-10, by wenzelm
tuned specifications of 'notation';
2007-11-10, by wenzelm
removed LocalTheory.target_naming/name;
2007-11-10, by wenzelm
put_inductives: be permissive about multiple versions
2007-11-10, by wenzelm
tuned proofs;
2007-11-10, by wenzelm
tuned document;
2007-11-10, by wenzelm
Orderings.min/max: no need to qualify consts;
2007-11-10, by wenzelm
auto_quickcheck ref: set default in ProofGeneral/preferences only
2007-11-10, by wenzelm
ProofGeneral/preferences: auto_quickcheck=true;
2007-11-10, by wenzelm
qualified Proofterm.proofs;
2007-11-10, by wenzelm
@{const}: improved ProofContext.read_const does the job;
2007-11-10, by wenzelm
locale_const: suppress in class body as well (prevents qualified printing);
2007-11-10, by wenzelm
notation: improved ProofContext.read_const does the job;
2007-11-10, by wenzelm
updated;
2007-11-10, by wenzelm
replaced @{const} (allows name only) by proper @{term};
2007-11-10, by wenzelm
proper implementation of check phase; non-qualified names for class operations
2007-11-09, by haftmann
explicit message for failed autoquickcheck
2007-11-09, by haftmann
tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;
2007-11-09, by wenzelm
avoid obsolete Sign.read_prop;
2007-11-09, by wenzelm
tuned proofs -- avoid implicit prems;
2007-11-09, by wenzelm
fixed imports path;
2007-11-09, by wenzelm
tuned proofs -- avoid open cases;
2007-11-09, by wenzelm
function package: using the names of the equations as case names turned out to be impractical => disabled
2007-11-09, by krauss
avoid name clashes when generating code for union, inter
2007-11-09, by krauss
oops -- avoid vacous goal message;
2007-11-08, by wenzelm
tuned messages;
2007-11-08, by wenzelm
avoid "import" as identifier, which is a keyword in Alice;
2007-11-08, by wenzelm
tuned presentation;
2007-11-08, by wenzelm
avoid implicit use of prems;
2007-11-08, by wenzelm
where/of: do not allow schematic variables here!
2007-11-08, by wenzelm
removed unused read_termTs_schematic, read/cert_vars_legacy, add_fixes_legacy;
2007-11-08, by wenzelm
discontinued legacy vars;
2007-11-08, by wenzelm
removed unused read_def_terms';
2007-11-08, by wenzelm
eliminated illegal schematic variables in where/of;
2007-11-08, by wenzelm
eliminated illegal schematic variables in where/of;
2007-11-08, by wenzelm
x86_64: fall back on x86 (more efficient);
2007-11-08, by wenzelm
tuned comments;
2007-11-08, by wenzelm
renamed ProofContext.read_const' to ProofContext.read_const_proper;
2007-11-08, by wenzelm
renamed ProofContext.read_const' to ProofContext.read_const_proper;
2007-11-08, by wenzelm
synchronize_syntax: improved declare_const (still inactive);
2007-11-08, by wenzelm
added const_proper;
2007-11-08, by wenzelm
added evaluation
2007-11-08, by nipkow
fix
2007-11-08, by nipkow
new general syntax
2007-11-08, by nipkow
tuned
2007-11-08, by nipkow
updated to notation and abbreviation
2007-11-08, by nipkow
added purify_sym
2007-11-08, by haftmann
tuned
2007-11-08, by haftmann
duv, mod, int conversion
2007-11-08, by haftmann
ProofContext.read_const';
2007-11-07, by wenzelm
Syntax.read_typ;
2007-11-07, by wenzelm
export read_const';
2007-11-07, by wenzelm
Syntax.read_typ;
2007-11-07, by wenzelm
added inductive
2007-11-07, by nipkow
attribute where/of: proper Syntax.parse/check;
2007-11-07, by wenzelm
discontinued ProofContext.read_prop_legacy;
2007-11-07, by wenzelm
discontinued ProofContext.read_prop_legacy;
2007-11-07, by wenzelm
refined Variable.declare_const;
2007-11-07, by wenzelm
refined notion of consts within the local scope;
2007-11-07, by wenzelm
tuned signature;
2007-11-07, by wenzelm
removed obsolete Sign.read_tyname/const (cf. ProofContext);
2007-11-07, by wenzelm
map and prefix
2007-11-07, by kleing
activated HOL-SizeChange;
2007-11-06, by wenzelm
tuned;
2007-11-06, by wenzelm
read_const/legacy_intern_skolem: cover consts within the local scope;
2007-11-06, by wenzelm
synchronize_syntax: declare operations within the local scope of fixes/consts
2007-11-06, by wenzelm
fixed spelling;
2007-11-06, by wenzelm
added is_const/declare_const for local scope of fixes/consts;
2007-11-06, by wenzelm
removed dependencies on Size_Change_Termination from HOL-Library;
2007-11-06, by wenzelm
moved stuff about size change termination to its own session
2007-11-06, by krauss
clarifying comment
2007-11-06, by haftmann
clarified merge
2007-11-06, by haftmann
Class.init now similiar to Locale.init
2007-11-06, by haftmann
CRITICAL force
2007-11-06, by haftmann
autoquickcheck message
2007-11-06, by haftmann
added explicit signature
2007-11-06, by haftmann
simplified specification of *_abs class
2007-11-06, by haftmann
tuned;
2007-11-06, by wenzelm
added autoquickcheck
2007-11-06, by haftmann
removed subclass edge ordered_ring < lordered_ring
2007-11-06, by haftmann