isabelle: Graph

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
rename approx_pd to pd_take
2008-07-01, by huffman
split Completion.thy from CompactBasis.thy
2008-07-01, by huffman
filemap for CVS -> Mercurial conversion;
2008-06-30, by wenzelm
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
2008-06-30, by huffman
New theory of deflations and embedding-projection pairs
2008-06-30, by huffman
remove unused Cset.thy
2008-06-30, by huffman
added facts to lemma swap_simps and tuned lemma calc_atms
2008-06-30, by urbanc
simplified retrieval of theory names of consts and types
2008-06-30, by haftmann
tagged arities
2008-06-30, by haftmann
HOL-Complex with proof terms
2008-06-30, by haftmann
code generator setup for "int" also works under eta-contraction
2008-06-30, by haftmann
added ML/ml_thms.ML;
2008-06-28, by wenzelm
tuned;
2008-06-28, by wenzelm
tuned;
2008-06-28, by wenzelm
additional ML antiquotations;
2008-06-28, by wenzelm
moved theorem values to ml_thms.ML;
2008-06-28, by wenzelm
Isar theorem values within ML.
2008-06-28, by wenzelm
added ML/ml_thms.ML;
2008-06-28, by wenzelm
updated generated file;
2008-06-28, by wenzelm
allow overlap of minor keywords and commands;
2008-06-28, by wenzelm
include HOL-Plain;
2008-06-28, by wenzelm
tuned args parser (cf. args.ML);
2008-06-28, by wenzelm
replaced simple_text by fully-featured parse_args;
2008-06-28, by wenzelm
tuned nested args parser;
2008-06-28, by wenzelm
@{lemma}: 'by' keyword;
2008-06-28, by wenzelm
ML: improved antiquotations;
2008-06-28, by wenzelm
added macro interface;
2008-06-28, by wenzelm
tuned;
2008-06-28, by wenzelm
added thm_name, opt_thm_name;
2008-06-28, by wenzelm
adjusted import
2008-06-27, by haftmann
adjusted import
2008-06-27, by haftmann
added a lemma to at_swap_simps
2008-06-27, by urbanc
remove cset theory; define ideal completions using typedef instead of cpodef
2008-06-26, by huffman
Args.theory;
2008-06-26, by wenzelm
added context/theory scanner;
2008-06-26, by wenzelm
Args.context;
2008-06-26, by wenzelm
fix: need to beta/eta normalize
2008-06-26, by krauss
established Plain theory and image
2008-06-26, by haftmann
added dummy citiation
2008-06-26, by haftmann
dropped recdef
2008-06-26, by haftmann
class theory name lookup improved
2008-06-26, by haftmann
modernized specifications;
2008-06-25, by wenzelm
tuned proofs;
2008-06-25, by wenzelm
modernized specifications;
2008-06-25, by wenzelm
modernized specifications;
2008-06-25, by wenzelm
typo
2008-06-25, by urbanc
re-use official outer keywords;
2008-06-25, by wenzelm
scan: prefer command over keyword, allowing lexicons to overlap;
2008-06-25, by wenzelm
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-25, by wenzelm
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-25, by wenzelm
antiquote: need to quote outer keywords;
2008-06-25, by wenzelm
tuned;
2008-06-25, by wenzelm
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
2008-06-25, by wenzelm
- Equivariance simpset used in proofs of strong induction and inversion
2008-06-25, by berghofe
pprint: back to proper output of markup, with workaround for Poly/ML crash;
2008-06-25, by wenzelm
back to 1.36 (Poly/ML crash!?);
2008-06-24, by wenzelm
updated generated file;
2008-06-24, by wenzelm
YXML: no special treatment of white space;
2008-06-24, by wenzelm
pprint: proper output of markup (important for token translation);
2008-06-24, by wenzelm
ml_code_antiq: proper scanner combinators;
2008-06-24, by wenzelm
moved concrete antiquotations to ml_antiquote.ML;
2008-06-24, by wenzelm
Antiquote.Open/Close;
2008-06-24, by wenzelm
add_antiq: more general notion of ML antiquotation;
2008-06-24, by wenzelm
added Open/Close -- checked blocks;
2008-06-24, by wenzelm
added pprint_thy_ref;
2008-06-24, by wenzelm
Common ML antiquotations.
2008-06-24, by wenzelm
added ML/ml_antiquote.ML;
2008-06-24, by wenzelm
ML_Antiquote.value;
2008-06-24, by wenzelm
added isaantiqopen/close;
2008-06-24, by wenzelm
Logic.all/mk_equals/mk_implies;
2008-06-23, by wenzelm
moved implies to logic.ML;
2008-06-23, by wenzelm
added all, is_all;
2008-06-23, by wenzelm
Logic.implies;
2008-06-23, by wenzelm
Logic.is_all;
2008-06-23, by wenzelm
Term.all;
2008-06-23, by wenzelm
Logic.all/mk_equals/mk_implies;
2008-06-23, by wenzelm
session name: empty for Pure and by default;
2008-06-23, by wenzelm
induct_tac: allow omission of arguments;
2008-06-23, by wenzelm
info: default name is "", not "Pure";
2008-06-23, by wenzelm
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
2008-06-23, by wenzelm
removed obsolete dest_concls;
2008-06-23, by wenzelm
induct_tac: mutual rules work as for method "induct";
2008-06-23, by wenzelm
tuned get_inductT: *all* rules for missing instantiation;
2008-06-23, by wenzelm
induct_tac: infer mutual rule from types, as for proper induct method;
2008-06-23, by wenzelm
induct_tac/case_tac: nested tuples are split as expected;
2008-06-23, by wenzelm
induct_tac: old conjunctive rules no longer supported;
2008-06-23, by wenzelm
updated generated file;
2008-06-23, by wenzelm
induct_tac: rule is inferred from types;
2008-06-23, by wenzelm
cleaned up some proofs;
2008-06-22, by huffman
use new-style abbreviation/notation for fix syntax
2008-06-22, by huffman
import_export_proof: simplified thm definition -- PureThy.name_thm does the job;
2008-06-21, by wenzelm
added query_type/const/class (meta data);
2008-06-21, by wenzelm
the_tags: explicit error message;
2008-06-21, by wenzelm
activate_context: strict the_context, no fallback on theory context;
2008-06-21, by wenzelm
remove unused constant liftpair
2008-06-20, by huffman
simplify profinite class axioms
2008-06-20, by huffman
clean up and rename some profinite lemmas
2008-06-20, by huffman
move at-sml-dev-e to macbroy23
2008-06-20, by isatest
replace SetPcpo.thy with Cset.thy
2008-06-20, by huffman
updated for 2008;
2008-06-20, by wenzelm
(removed non-present change)
2008-06-20, by haftmann
explicit thm context for error messages
2008-06-20, by haftmann
using tages to find theory names
2008-06-20, by haftmann
type constructors now with markup
2008-06-20, by haftmann
fixed bind error for malformed primrec specifications
2008-06-20, by haftmann
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
2008-06-20, by haftmann
streamlined definitions
2008-06-20, by haftmann
moved Float.thy to Library
2008-06-20, by haftmann
removed SetPcpo.thy and cpo instance for type bool;
2008-06-20, by huffman
moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale
2008-06-20, by huffman
add lemma Abs_image
2008-06-20, by huffman
added some lemmas; reorganized into sections; tuned proofs
2008-06-20, by huffman
added some lemmas; tuned proofs
2008-06-20, by huffman
tuned
2008-06-20, by huffman
replace less_lift with flat_less_iff
2008-06-20, by huffman
tweak lemmas adm_all and adm_ball
2008-06-20, by huffman
move lemmas into locales;
2008-06-19, by huffman
add lemmas take_chain_less and take_chain_le
2008-06-19, by huffman