Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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
Tuned and simplified proofs
2008-07-21, by chaieb
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra
2008-07-21, by chaieb
Relevant rules added to algebra's context
2008-07-21, by chaieb
renamed item to span, renamed contructors;
2008-07-20, by wenzelm
adapted ThyEdit.span;
2008-07-20, by wenzelm
maintain token range;
2008-07-20, by wenzelm
tty loop: do not report status;
2008-07-20, by wenzelm
added type range;
2008-07-20, by wenzelm
renamed command span markup;
2008-07-20, by wenzelm
SideKickParsedData: minimal content;
2008-07-20, by wenzelm
(adjusted)
2008-07-20, by haftmann
(adjusted)
2008-07-20, by haftmann
added verification framework for the HeapMonad and quicksort as example for this framework
2008-07-19, by bulwahn
build jedit plugin only if jedit is available;
2008-07-19, by wenzelm
misc tuning;
2008-07-18, by wenzelm
more class instantiations
2008-07-18, by haftmann
refined code generator setup for rational numbers; more simplification rules for rational numbers
2008-07-18, by haftmann
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-07-18, by haftmann
fixed Scala path;
2008-07-18, by wenzelm
tuned build order;
2008-07-17, by wenzelm
proper purge_tmp;
2008-07-17, by wenzelm
tuned message;
2008-07-17, by wenzelm
tuned line breaks (NB: generated text is inserted here);
2008-07-17, by wenzelm
proper usage message;
2008-07-17, by wenzelm
make Isabelle source distribution (via Mercurial);
2008-07-17, by wenzelm
explicit Distribution.changelog;
2008-07-17, by wenzelm
structure Distribution: swapped default for is_official;
2008-07-17, by wenzelm
ThyInfo.remove_thy;
2008-07-17, by wenzelm
structure Distribution: swapped default for is_official;
2008-07-17, by wenzelm
use ../isabelle.sty and ../isabellesym.sty;
2008-07-17, by wenzelm
tuned whitespace;
2008-07-17, by wenzelm
removed old checklist;
2008-07-17, by wenzelm
obsolete;
2008-07-17, by wenzelm
tuned;
2008-07-17, by wenzelm
discontinued maketags;
2008-07-17, by wenzelm
assume GNU tar and find;
2008-07-17, by wenzelm
tuned;
2008-07-17, by wenzelm
use ../isabellesym.sty, which is always available;
2008-07-17, by wenzelm
Admin/build browser;
2008-07-17, by wenzelm
less verbosity;
2008-07-17, by wenzelm
Administrative build -- finish Isabelle source distribution.
2008-07-17, by wenzelm
simplified proofs
2008-07-17, by krauss
beautified proofs
2008-07-17, by nipkow
added lemmas
2008-07-17, by nipkow
Added Standardization theory to nominal examples.
2008-07-16, by berghofe
Added Standardization theory.
2008-07-16, by berghofe
editor model: run interactively for now;
2008-07-16, by wenzelm
updated generated file;
2008-07-16, by wenzelm
identify: more informative id in Toplevel.debug mode;
2008-07-16, by wenzelm
shortlogentry/filelogentry: show shortdate and full description;
2008-07-16, by wenzelm
Removed uses of context element includes.
2008-07-16, by ballarin
added Isar.command, Isar.insert, Isar.remove (editor model);
2008-07-16, by wenzelm
export type id with no_id and create_command;
2008-07-16, by wenzelm
tuned;
2008-07-15, by wenzelm
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
2008-07-15, by wenzelm
load thy_edit.ML before isar.ML;
2008-07-15, by wenzelm
modernized specifications and proofs;
2008-07-15, by wenzelm
Removed uses of context element includes.
2008-07-15, by ballarin
tuned
2008-07-15, by haftmann
tuned code theorem bookkeeping
2008-07-15, by haftmann
tuned changelogentry;
2008-07-15, by wenzelm
refined Output.status_fn: priority (only visible for non-empty output, e.g. via test_markup print mode);
2008-07-15, by wenzelm
support for command status;
2008-07-15, by wenzelm
added status channel;
2008-07-15, by wenzelm
added status channel;
2008-07-15, by wenzelm
tuned;
2008-07-15, by wenzelm
simplified commit_exit;
2008-07-15, by wenzelm
simplified commit_exit: operate on previous node of final state, include warning here;
2008-07-15, by wenzelm
removed obsolete commit_exit;
2008-07-15, by wenzelm
added command 'linear_undo';
2008-07-15, by wenzelm
removed command 'redo';
2008-07-15, by wenzelm
adapted ThyInfo.end_theory;
2008-07-15, by wenzelm
dropped map; fixed swap
2008-07-15, by haftmann
curried gcd
2008-07-15, by haftmann
cover macbroy as well;
2008-07-14, by wenzelm
tuned filelogentry;
2008-07-14, by wenzelm
print_mode "test_markup": do not change prompt, otherwise Proof General will not work;
2008-07-14, by wenzelm
tuned message;
2008-07-14, by wenzelm
updated generated file;
2008-07-14, by wenzelm
inform_file_processed: Isar.init_point last!
2008-07-14, by wenzelm
removed HOL-Complex, which has been discontinued after Isabelle2008;
2008-07-14, by wenzelm
added HOL-Nominal image;
2008-07-14, by wenzelm
removed obsolete Pure/General/history.ML;
2008-07-14, by wenzelm
inform_file_processed: try harder not to fail, ensure
2008-07-14, by wenzelm
commit_exit: proper error;
2008-07-14, by wenzelm
export EXCURSION_FAIL;
2008-07-14, by wenzelm
dropped junk
2008-07-14, by haftmann
moved bootstrap of simplifier
2008-07-14, by haftmann
tuned
2008-07-14, by haftmann
end_theory: no result;
2008-07-14, by wenzelm
removed obsolete Toplevel.RESTART;
2008-07-14, by wenzelm
proper_inform_file_processed: new implementation based on global Isar state (cf. isar.ML);
2008-07-14, by wenzelm
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
2008-07-14, by wenzelm
adapted IsarCmd.init_theory;
2008-07-14, by wenzelm
renamed theory to init_theory, removed obsolete kill argument;
2008-07-14, by wenzelm
added commit_exit;
2008-07-14, by wenzelm
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
2008-07-14, by krauss
renamed conversions to _conv, tuned
2008-07-14, by krauss
Simplified proofs
2008-07-14, by chaieb
Simple theorems about zgcd moved to GCD.thy
2008-07-14, by chaieb
Theorem names as in IntPrimes.thy, also several theorems moved from there
2008-07-14, by chaieb
Fixed proofs.
2008-07-14, by chaieb
ProofNode.current
2008-07-14, by wenzelm
command 'redo' no longer available;
2008-07-14, by wenzelm
replaced obsolete ProofHistory by ProofNode (backtracking only);
2008-07-14, by wenzelm
removed obsolete 'redo' command;
2008-07-14, by wenzelm
removed obsolete history commands;
2008-07-14, by wenzelm
Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
2008-07-14, by wenzelm
obsolete (cf. proof_node.ML);
2008-07-14, by wenzelm
removed Isar/proof_history.ML;
2008-07-14, by wenzelm
added further simple interfaces
2008-07-14, by haftmann
simpsets as pre/postprocessors; generic preprocessor now named function transformators
2008-07-14, by haftmann
unified curried gcd, lcm, zgcd, zlcm
2008-07-14, by haftmann
Sorts.weaken: abstract argument;
2008-07-11, by wenzelm
Sorts.weaken: abstract argument;
2008-07-11, by wenzelm
instance real_field < field_char_0;
2008-07-11, by huffman
re-removed subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef
2008-07-11, by haftmann
Fract now total; improved code generator setup
2008-07-11, by haftmann
simple inheritance concept
2008-07-11, by haftmann
tuned thyname lookup
2008-07-11, by haftmann
fixed layout
2008-07-11, by haftmann
explicit completions of arities
2008-07-11, by haftmann
tuned order
2008-07-11, by haftmann
antiquotation
2008-07-11, by haftmann
improved code generator setup
2008-07-11, by haftmann
explicit dependency
2008-07-11, by haftmann
class instead of axclass
2008-07-11, by haftmann
tuned import
2008-07-11, by haftmann
separate class dvd for divisibility predicate
2008-07-11, by haftmann
temporarily disable at-sml-dev-p
2008-07-11, by kleing
updated generated file;
2008-07-10, by wenzelm
restart: Isar.init_point;
2008-07-10, by wenzelm
proper_inform_file_processed: Isar.init_point starts fresh command sequence;
2008-07-10, by wenzelm
activated new versions of undo, kill_proof;
2008-07-10, by wenzelm
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
2008-07-10, by wenzelm
added print;
2008-07-10, by wenzelm
added ProofGeneral.isar_kill_proof;
2008-07-10, by wenzelm
added Isar.init_point, Isar.kill;
2008-07-10, by wenzelm
export init_point;
2008-07-10, by wenzelm
added Isar.linear_undo;
2008-07-10, by wenzelm
tuned;
2008-07-10, by wenzelm
tty interaction: do not move point after error;
2008-07-10, by wenzelm
change_lexicons: no verbosity;
2008-07-10, by wenzelm
added Isar.undo, which emulates old-style undo on global tty state;
2008-07-10, by wenzelm
provide old-style undo operation (still unused);
2008-07-10, by wenzelm
added prompt markup;
2008-07-10, by wenzelm
@{lemma}: allow terminal method;
2008-07-10, by wenzelm
@{lemma}: allow terminal method, close derivation unless (open) mode is given;
2008-07-10, by wenzelm
added is_diag;
2008-07-10, by wenzelm
slightly improved @{lemma} (both for latex and ML);
2008-07-10, by wenzelm
misc tuning;
2008-07-10, by wenzelm
Fixed (harmless) typo in closing *}.
2008-07-10, by ballarin
by intro_locales -> ..
2008-07-10, by huffman
instance real_field < field_char_0
2008-07-10, by huffman
remove redundant lemmas about cmod
2008-07-09, by huffman
removed owner;
2008-07-09, by wenzelm
tuned description;
2008-07-09, by wenzelm
changes wrt. gitweb style;
2008-07-09, by wenzelm
style = isabelle (based on gitweb);
2008-07-09, by wenzelm
rearrange instantiations
2008-07-09, by huffman
added get_first;
2008-07-09, by wenzelm
updated generated file;
2008-07-08, by wenzelm
updated generated file;
2008-07-08, by wenzelm
fix more typos
2008-07-08, by huffman
fix another typo
2008-07-08, by huffman
fix typo
2008-07-08, by huffman
updated generated file;
2008-07-08, by wenzelm
global commands: explicit graph;
2008-07-08, by wenzelm
export str_of;
2008-07-08, by wenzelm
clarified code
2008-07-08, by haftmann
exported weaken combinator
2008-07-08, by haftmann
refined arity property concept
2008-07-08, by haftmann
fix: using IntInf.int for SML
2008-07-08, by haftmann
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
2008-07-08, by wenzelm
removed obsolete touch_child_thys;
2008-07-08, by wenzelm
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
2008-07-08, by wenzelm
more qualified ThyInfo names;
2008-07-08, by wenzelm
begin_theory: files_html needs to be produced outside of prep_html_source to make ML files appear!
2008-07-08, by wenzelm
removed unused href_opt_name;
2008-07-08, by wenzelm
migrated at-sml-dev-p to macbroy24, hoping for more reliable hardware
2008-07-08, by kleing
retired mac-sml-dev.
2008-07-07, by kleing
absolute imports of HOL/*.thy theories
2008-07-07, by haftmann
prefer theorem names without numbers
2008-07-04, by huffman
HOL-NSA
2008-07-04, by huffman
added marginal setup for code generation
2008-07-04, by haftmann
use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero
2008-07-03, by huffman
removed old NSPrimes, cf. NSA/Examples/;
2008-07-03, by wenzelm
cvsps: back to non-verbose mode;
2008-07-03, by wenzelm
removed old Complex/ex/NSPrimes.thy;
2008-07-03, by wenzelm
maxfiles = 50;
2008-07-03, by wenzelm
more sessions;
2008-07-03, by wenzelm
more precise dependencies for HOL-Word and HOL-NSA;
2008-07-03, by wenzelm
fixed extremely slow proof of Chain_inits_DiffI
2008-07-03, by huffman
add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)
2008-07-03, by huffman
move proofs of add_left_cancel and add_right_cancel into the correct locale
2008-07-03, by huffman
cvsps -v (verbose);
2008-07-03, by wenzelm
removed nonstandard analysis theories to HOL-NSA
2008-07-03, by huffman
moved theories to HOL/NSA
2008-07-03, by huffman
add HOL-NSA
2008-07-03, by huffman
use patched cvsps to workaround loss of "foo: bar;" log entries;
2008-07-03, by wenzelm
move nonstandard analysis theories to NSA directory
2008-07-03, by huffman
back to default style, which shows files in changelog view;
2008-07-03, by wenzelm
added description;
2008-07-03, by wenzelm
tuned;
2008-07-03, by wenzelm
logrotate setup;
2008-07-03, by wenzelm
redirect stderr as well;
2008-07-03, by wenzelm
output to log file;
2008-07-03, by wenzelm
specific to CVS;
2008-07-03, by wenzelm
Isabelle repository service.
2008-07-03, by wenzelm
ensure hg/.hg/hgrc;
2008-07-03, by wenzelm
hgrc for conversion and web service;
2008-07-03, by wenzelm
provide HGRCPATH, taken from cvs/Admin;
2008-07-03, by wenzelm
code antiquotation roaring ahead
2008-07-03, by haftmann
tuned
2008-07-03, by haftmann
adjusted postprocessort setup
2008-07-03, by haftmann
added lemma antiquotation
2008-07-03, by haftmann
adjusted rep_datatype
2008-07-03, by haftmann
Adapted to changes in perm_simp / swap_simps.
2008-07-03, by berghofe
Replaced all but one occurrence of perm_simp_tac by perm_simproc_app,
2008-07-03, by berghofe
Rewrote code to use swap_simps rather than calc_atm (which tends to
2008-07-03, by berghofe
moved HOL-Plain up;
2008-07-02, by wenzelm
rename Doc doc-src;
2008-07-02, by wenzelm
renamed Contents to Dirs to avoid case-conflict with doc/Contents;
2008-07-02, by wenzelm
section -> subsection
2008-07-02, by huffman
convert Isabelle CVS to Mercurial;
2008-07-02, by wenzelm
use begin and end for proofs in locales
2008-07-02, by huffman
exclude Distribution/bin/Isabelle;
2008-07-02, by wenzelm
init_theory: pass name explicitly;
2008-07-02, by wenzelm
replaced datatype category constructivism by is_theory/is_proof;
2008-07-02, by wenzelm
Toplevel.init_theory: pass name explicitly;
2008-07-02, by wenzelm
command: always keep transition, not just as initial status;
2008-07-02, by wenzelm
cached code for code antiquotation
2008-07-02, by haftmann
code antiquotation roaring ahead
2008-07-02, by haftmann
cleaned up some code generator configuration
2008-07-02, by haftmann
tuned;
2008-07-01, by wenzelm
added datatype category;
2008-07-01, by wenzelm
replaced datatype kind by OuterKeyword.category;
2008-07-01, by wenzelm
clean: HOL-Plain;
2008-07-01, by wenzelm
prove lemma finite in context of finite class
2008-07-01, by huffman
added HOL-Plain;
2008-07-01, by wenzelm
explicit identification of toplevel commands, with status etc.;
2008-07-01, by wenzelm
added name_of;
2008-07-01, by wenzelm
added get_id/put_id;
2008-07-01, by wenzelm
(removed Complex/ROOT.ML)
2008-07-01, by haftmann
HOL += HOL-Complex
2008-07-01, by haftmann
HOL += HOL-Complex
2008-07-01, by haftmann
tuned
2008-07-01, by haftmann
HOL += HOL-Complex
2008-07-01, by haftmann
put file dependencies on separate lines
2008-07-01, by huffman
range_composition no longer in simp set
2008-07-01, by huffman
remove simp attribute from range_composition
2008-07-01, by huffman
rename INF to INFM
2008-07-01, by huffman
remove unused lemmas ub2ub_monofun' and dir2dir_monofun
2008-07-01, by huffman
remove redundant instance proof finite_po < cpo
2008-07-01, by huffman
remove unused lemma is_lub_Iup'
2008-07-01, by huffman
replace lub (range Y) with (LUB i. Y i)
2008-07-01, by huffman
add file dependencies
2008-07-01, by huffman
universal bifinite domain
2008-07-01, by huffman
isomorphisms between naturals and sums, products, and finite sets
2008-07-01, by huffman
theory of algebraic deflations
2008-07-01, by huffman
theory of eventually-constant sequences
2008-07-01, by huffman
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
2008-07-01, by huffman
rename compact_approx to compact_take
2008-07-01, by huffman
less
more
|
(0)
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip