isabelle: Graph

removed separate logtypes field of syntax;
2004-06-09, by wenzelm
Path.split_ext; more robust inform_file_processed;
2004-06-09, by wenzelm
Sign.is_logtype;
2004-06-09, by wenzelm
Syntax.default_mode;
2004-06-09, by wenzelm
added option 'locale=NAME';
2004-06-09, by wenzelm
Url.File;
2004-06-09, by wenzelm
* Document preparation: antiquotations provide option 'locale=NAME';
2004-06-09, by wenzelm
tuned comment;
2004-06-09, by wenzelm
updated/tuned identifier syntax;
2004-06-09, by wenzelm
updated notes on sub-/superscripts;
2004-06-09, by wenzelm
removed Syntax.test_read;
2004-06-09, by wenzelm
added a lemma lfp_ordinal_induct
2004-06-09, by nipkow
fixed the groupI ambiguity
2004-06-09, by paulson
fixed the skolemize method
2004-06-09, by paulson
moved some cardinality results into main HOL
2004-06-09, by paulson
add_dummies no longer uses transform_error but handles specific
2004-06-08, by berghofe
Added exception Datatype_Empty.
2004-06-08, by berghofe
mk_id is now also applied to identifiers in test_term.
2004-06-08, by berghofe
Groups, Rings and supporting lemmas in ZF
2004-06-08, by paulson
Groups, Rings and supporting lemmas
2004-06-08, by paulson
Groups, Rings and supporting lemmas
2004-06-08, by paulson
avoid Args.list (lost update?);
2004-06-06, by wenzelm
added has_mode; handle_error: output raw;
2004-06-06, by wenzelm
Symbol.output;
2004-06-06, by wenzelm
no token translation / setup for Latex;
2004-06-06, by wenzelm
HOL: symbolic syntax of Eps;
2004-06-06, by wenzelm
More readable code.
2004-06-05, by chaieb
pretty_thm/goals_aux, pretty_flexpair: pp;
2004-06-05, by wenzelm
avoid implicit arguments via refs;
2004-06-05, by wenzelm
Symbol.decode;
2004-06-05, by wenzelm
added datatype sym, val decode: symbol -> sym;
2004-06-05, by wenzelm
improved symbolic syntax of Eps: \<some> for mode "epsilon";
2004-06-05, by wenzelm
removed mlworks and smlnj-0.93 (obsolete);
2004-06-05, by wenzelm
tuned comments;
2004-06-05, by wenzelm
moved exception handling back to library.ML;
2004-06-05, by wenzelm
tuned exeption handling (capture/release);
2004-06-05, by wenzelm
removed Pure/ML-Systems/mlworks.ML Pure/ML-Systems/polyml-3.x.ML Pure/ML-Systems/smlnj-0.93.ML; added ML-Systems/polyml-time-limit.ML;
2004-06-05, by wenzelm
obsolete;
2004-06-05, by wenzelm
Tuned parse_att.
2004-06-04, by berghofe
new rules for simplifying quantifiers with Sigma
2004-06-02, by paulson
Add alternative syntax for attributes
2004-06-01, by aspinall
Add panic function which exits Isabelle immediately.
2004-06-01, by aspinall
Removed ~10000 hack in function idx that can lead to inconsistencies
2004-06-01, by berghofe
Adapted to new name mangling function in code generator.
2004-06-01, by berghofe
Adapted to new name mangling function.
2004-06-01, by berghofe
Improved name mangling function.
2004-06-01, by berghofe
proper use of 'nonterminals';
2004-06-01, by wenzelm
proper treatment of logical types within syntax;
2004-06-01, by wenzelm
removed obsolete sort 'logic' and '=?=' syntax;
2004-06-01, by wenzelm
removed obsolete sort 'logic';
2004-06-01, by wenzelm
more on bij_betw
2004-06-01, by paulson
tidied
2004-06-01, by paulson
TimeLimit structure added (no proper implementation yet)
2004-06-01, by webertj
including polyml-time-limit.ML
2004-06-01, by webertj
SML/NJs TimeLimit structure ported to Poly/ML
2004-06-01, by webertj
oops -- no Output.out here;
2004-05-31, by wenzelm
updated;
2004-05-29, by wenzelm
\<^bsub>/\<^esub> syntax: unbreakable block;
2004-05-29, by wenzelm
\<^bsub>/\<^esub> syntax: unbreakable block;
2004-05-29, by wenzelm
Scan.this; tuned;
2004-05-29, by wenzelm
do *not* export list/list1 -- commas considered special in arg syntax;
2004-05-29, by wenzelm
target 'generate';
2004-05-29, by wenzelm
avoid Args.list;
2004-05-29, by wenzelm
handle raw symbols; Output.add_mode;
2004-05-29, by wenzelm
handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
2004-05-29, by wenzelm
tuned _dummy_ofsort syntax;
2004-05-29, by wenzelm
added pp_show_brackets; support unbreakable blocks;
2004-05-29, by wenzelm
transform_error;
2004-05-29, by wenzelm
Library.read_int; Output.output;
2004-05-29, by wenzelm
improved support for raw symbols;
2004-05-29, by wenzelm
Output.error;
2004-05-29, by wenzelm
pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
2004-05-29, by wenzelm
added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;
2004-05-29, by wenzelm
removed norm_typ; improved output; refer to Pretty.pp;
2004-05-29, by wenzelm
moved read_int etc. to library.ML; added type 'arity';
2004-05-29, by wenzelm
improved output; refer to Pretty.pp;
2004-05-29, by wenzelm
Output.add_mode; Output.timing;
2004-05-29, by wenzelm
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
2004-05-29, by wenzelm
Output.timing;
2004-05-29, by wenzelm
improved output;
2004-05-29, by wenzelm
moved print_mode to General/output.ML; load General/pretty.ML early;
2004-05-29, by wenzelm
added Pure/General/output.ML;
2004-05-29, by wenzelm
avoid 'handle _' -- would cover Interrupt as well!!!
2004-05-29, by wenzelm
Sign.infer_types: Sign.pp;
2004-05-29, by wenzelm
Library.read_int;
2004-05-29, by wenzelm
Output.output;
2004-05-29, by wenzelm
'classrel': support multiple arguments;
2004-05-29, by wenzelm
* ML: all output via channels of writeln etc. passed through Output.output;
2004-05-29, by wenzelm
output channels;
2004-05-29, by wenzelm
added asm_lr_simplify/asm_lr_rewrite and adapted asm_full_simplify/asm_full_rewrite to match to corresponding simp_tacs
2004-05-28, by schirmer
new skolemize_tac and skolemize method
2004-05-28, by paulson
new theorem Collect_imp_eq
2004-05-28, by paulson
abstraction over functions is no default any more.
2004-05-26, by chaieb
adjusted for different signature of Type.typ_instance
2004-05-26, by webertj
mainly new/different datatype examples
2004-05-26, by webertj
documentation updated
2004-05-26, by webertj
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
2004-05-26, by webertj
new default parameters for refute
2004-05-26, by webertj
solver "auto" now issues a warning when it uses solver "enumerate"
2004-05-26, by webertj
Corrected printer bug for bounded quantifiers Q x<=y. P
2004-05-26, by nipkow
more group isomorphisms
2004-05-26, by paulson
added drop_take:thm
2004-05-24, by nipkow
- deleted unneeded function eta_long (now in Pure/pattern.ML
2004-05-21, by berghofe
Adapted to new syntax for case expressions.
2004-05-21, by berghofe
Added more flexible parse / print translations for case expressions.
2004-05-21, by berghofe
Modified functions pt_to_ast and ast_to_term to improve handling
2004-05-21, by berghofe
- exported result datatype
2004-05-21, by berghofe
updated;
2004-05-21, by wenzelm
Pure: clear separation of logical types and nonterminals;
2004-05-21, by wenzelm
adapted tsig/sg interface;
2004-05-21, by wenzelm
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
2004-05-21, by wenzelm
added fold, product; removed transitive_closure;
2004-05-21, by wenzelm
adapted names of some sort ops;
2004-05-21, by wenzelm
major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;
2004-05-21, by wenzelm
Type.strip_sorts;
2004-05-21, by wenzelm
incorporate type inference interface from type.ML;
2004-05-21, by wenzelm
adapted tsig interface;
2004-05-21, by wenzelm
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
2004-05-21, by wenzelm
test_classrel/arity improve error reporting; tuned;
2004-05-21, by wenzelm
xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;
2004-05-21, by wenzelm
string_of_vname moved to term.ML;
2004-05-21, by wenzelm
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
2004-05-21, by wenzelm
type.ML now before Syntax module;
2004-05-21, by wenzelm
xxx_typ_raw replace xxx_typ_no_norm forms;
2004-05-21, by wenzelm
'classrel' now allows multiple arguments;
2004-05-21, by wenzelm
Sign.certify_tyname;
2004-05-21, by wenzelm
TypeInfer.paramify_dummies, TypeInfer.param;
2004-05-21, by wenzelm
Args.local_typ_raw;
2004-05-21, by wenzelm
output_tym: removed duplicate clauses;
2004-05-21, by wenzelm
Graph.minimals;
2004-05-21, by wenzelm
adapted syntax to cope with lack of non-logical types;
2004-05-21, by wenzelm
Type.typ_instance;
2004-05-21, by wenzelm
load ML files only once;
2004-05-21, by wenzelm
removed duplicate thms;
2004-05-21, by wenzelm
Sign.typ_instance;
2004-05-21, by wenzelm
tuned message;
2004-05-21, by wenzelm
tuned document;
2004-05-21, by wenzelm
use plain SOME;
2004-05-21, by wenzelm
proper use of 'syntax';
2004-05-21, by wenzelm
auto update
2004-05-19, by paulson
has_consts now handles the @-operator
2004-05-19, by paulson
new bij_betw operator
2004-05-19, by paulson
more results about isomorphisms
2004-05-19, by paulson
conversion of Hilbert_Choice to Isar script
2004-05-19, by paulson
the function list1 has been exported.
2004-05-19, by chaieb
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
2004-05-19, by chaieb
tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger.
2004-05-19, by chaieb
modified abel_cancel.ML for polymorphic types
2004-05-18, by obua
simplification for abelian groups
2004-05-18, by obua
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
2004-05-18, by obua
Comments fixed
2004-05-17, by webertj
lemma disjoint_int_union removed - too special
2004-05-17, by mehta
Change of theory hierarchy: Group is now based in Lattice.
2004-05-14, by ballarin
tidied
2004-05-14, by paulson
new atomize theorem
2004-05-14, by paulson
removed a premise of card_inj_on_le
2004-05-14, by paulson
removal of locale coset
2004-05-14, by paulson
deleted redundant proof lines
2004-05-14, by paulson
new lemmas
2004-05-14, by paulson
clauses for ordinary resolution
2004-05-14, by paulson
conversion of theorems to atomic form
2004-05-14, by paulson
New simp rules added:
2004-05-13, by mehta
simpilified and strengthened proofs
2004-05-12, by paulson
fixed latex problems
2004-05-12, by nipkow
renamed `> to o_m
2004-05-12, by nipkow
changes made due to new Ring_and_Field theory
2004-05-11, by obua
Eta-expanded function scan_comment to make SmlNJ happy.
2004-05-11, by berghofe
broken no longer includes TTP, and other minor changes
2004-05-11, by paulson
removal of prime characters
2004-05-11, by paulson
package needed for superscripts
2004-05-11, by paulson
conversion to clauses for ordinary resolution rather than ME
2004-05-11, by paulson
auto update
2004-05-11, by paulson
Pure: nested comments in inner syntax;
2004-05-10, by wenzelm
support nested comments;
2004-05-10, by wenzelm
changed Symbol.beginning;
2004-05-10, by wenzelm
tuned;
2004-05-10, by wenzelm
Source.of_list: no buffer limitation (now pointless due to tail-recursive Scan.repeat);
2004-05-10, by wenzelm
added Scan.list;
2004-05-10, by wenzelm
ProofGeneral.process_pgip command;
2004-05-10, by wenzelm
preparation for integration with new Ring_and_Field.thy
2004-05-10, by obua
moved first lemma in LongDiv.ML to LongDiv.thy
2004-05-10, by obua
replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
2004-05-09, by obua
removed Aux.thy;
2004-05-09, by bauerg
cleanup up read functions, include liberal versions;
2004-05-07, by wenzelm
be liberal about constant names;
2004-05-07, by wenzelm
tuned;
2004-05-07, by wenzelm
tuned notation;
2004-05-07, by wenzelm
tuned document;
2004-05-07, by wenzelm
*** empty log message ***
2004-05-07, by bauerg
Add FIXME note re FAIL (is it fixed yet?)
2004-05-07, by aspinall
Add cdata output. Add tabs in whitespace. Write two strings instead of Library.quote.
2004-05-07, by aspinall
Add -X option to trigger PGIP interaction mode.
2004-05-07, by aspinall
*** empty log message ***
2004-05-07, by bauerg
replaced Aux.thy by RealLemmas.thy
2004-05-07, by bauerg
tuned HOL/record package; enabled record_upd_simproc by default.
2004-05-06, by schirmer
improved block sup/sub;
2004-05-06, by wenzelm
show_structs option;
2004-05-06, by wenzelm
tuned document;
2004-05-06, by wenzelm
tidied
2004-05-06, by paulson
auto update
2004-05-06, by paulson
redundant clause removed
2004-05-04, by webertj
solved sml-nj compatibility problem
2004-05-04, by schirmer
tuned;
2004-05-04, by schirmer
reimplementation of HOL records; only one type is created for
2004-05-03, by schirmer
tuned;
2004-05-01, by wenzelm
improvd indexed syntax and implicit structures; tuned renaming of symbolic identifiers
2004-05-01, by wenzelm
improved indexed syntax / implicit structures;
2004-05-01, by wenzelm
tuned;
2004-05-01, by wenzelm
improved Term.invent_names;
2004-05-01, by wenzelm
removed 'constdefs' hack;
2004-05-01, by wenzelm
improved syntax;
2004-05-01, by wenzelm
improved subscript syntax;
2004-05-01, by wenzelm
tuned instance statements;
2004-05-01, by wenzelm
_index1: accomodate improved indexed syntax;
2004-05-01, by wenzelm
breaks flag;
2004-05-01, by wenzelm
warning: non-identifier declaration;
2004-04-29, by wenzelm
added is_keyword;
2004-04-29, by wenzelm
added is_literal;
2004-04-29, by wenzelm
more robust output of definitions;
2004-04-29, by wenzelm
removed 'constdefs' hack;
2004-04-29, by wenzelm
removed spurious quick_and_dirty;
2004-04-29, by wenzelm
HOLCF: discontinued special version of 'constdefs';
2004-04-29, by wenzelm
comments modified
2004-04-28, by webertj
use Syntax.is_ascii_identifier;
2004-04-26, by wenzelm
added is_ascii_identifier;
2004-04-26, by wenzelm
clarification of ascii vs. symbolic entities;
2004-04-26, by wenzelm
tuned presentation;
2004-04-26, by wenzelm
variant: use Symbol.bump_init;
2004-04-26, by wenzelm
removed obsolete 'undo';
2004-04-26, by wenzelm
*** empty log message ***
2004-04-26, by wenzelm
use Syntax.is_identifier;
2004-04-26, by wenzelm
use ThmDatabase.is_ml_identifier;
2004-04-26, by wenzelm
added isasymsome;
2004-04-26, by wenzelm
add solaris and darwin
2004-04-26, by kleing
commented
2004-04-26, by paulson
Isabelle on windoze
2004-04-26, by kleing
added AFP
2004-04-26, by kleing
improved notation;
2004-04-23, by wenzelm
index syntax: support for general expressions (input only);
2004-04-23, by wenzelm
improved messages;
2004-04-23, by wenzelm
HOL-Matrix: document setup;
2004-04-23, by wenzelm
proper document setup;
2004-04-23, by wenzelm
tuned notation;
2004-04-23, by wenzelm
updated -- too late for Isabelle2004!
2004-04-23, by wenzelm
add link to HOL4 libraries
2004-04-23, by kleing
congruent2 now allows different equiv relations
2004-04-23, by paulson
'constdefs' with automatic type-inference and structure context;
2004-04-22, by wenzelm
changed SML/NJ v 45 to 44
2004-04-22, by paulson
Pure: considerably improved version of 'constdefs' command;
2004-04-22, by wenzelm
fixed constdefs typing;
2004-04-22, by wenzelm
constdefs: proper order;
2004-04-22, by wenzelm
tmp hack get back to old 'constdefs';
2004-04-22, by wenzelm
improved notation;
2004-04-22, by wenzelm
added Isar/constdefs.ML;
2004-04-22, by wenzelm
removed add_constdefs(_i), see constdefs.ML for improved version; advanced translation functions;
2004-04-22, by wenzelm
tuned interfaces to accomodate advanced translation functions;
2004-04-22, by wenzelm
non_typed_tr';
2004-04-22, by wenzelm
added opt_keyword, mixfix';
2004-04-22, by wenzelm
support for advanced translation functions;
2004-04-22, by wenzelm
adapted Sign.rep_sg;
2004-04-22, by wenzelm
tuned;
2004-04-22, by wenzelm
improved constdefs and translation functions;
2004-04-22, by wenzelm
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
2004-04-22, by paulson
new lemmas
2004-04-22, by paulson
typo
2004-04-22, by kleing
Higher order logic more obvious than set theory
2004-04-22, by kleing
removed 'tutorial out now' (out of date)
2004-04-22, by kleing
added GNU Emacs, fixed x-symbol enabling (Options menu, not Customize)
2004-04-22, by kleing
now included in Complex/README.html
2004-04-21, by paulson
fixed to include Real and Hyperreal
2004-04-21, by paulson
add HOL4 image, needs fixing
2004-04-20, by kleing
temporarily reverted quote change for release. breaks latex output, needs more testing. Isabelle2004_0
2004-04-19, by kleing
badly-needed updates
2004-04-19, by paulson
inlcude HOL proof terms and HOL4 image
2004-04-19, by kleing
fixed address
2004-04-19, by paulson
fixed address
2004-04-19, by paulson
Forgot a couple of checks for the quick_and_dirty flag the other day.
2004-04-19, by skalberg
renamed HOL-Import-HOL to HOL4, added to images target
2004-04-19, by kleing
change quote to Library.quote, fixes LaTeX \isarchardoublequote problem.
2004-04-19, by kleing
add HOL4
2004-04-19, by kleing
devel snapshot is now tested
2004-04-19, by kleing
updated Tobias' address
2004-04-19, by kleing
Whoops, forgot a header...
2004-04-17, by skalberg
Minor cleanup of headers and some speedup of the HOL4 import.
2004-04-17, by skalberg
Added documentation for ax_specification, as well as a small comparison of
2004-04-17, by skalberg
Fixed bug in rmod that caused an overflow exception in SML/NJ.
2004-04-17, by berghofe
Added case distinction proof pattern.
2004-04-17, by nipkow
added sydney mirror
2004-04-17, by kleing
small additions
2004-04-17, by nipkow
2003 -> 2004
2004-04-17, by nipkow
do not mention poly 3.x any more (it is untested)
2004-04-17, by kleing
do not mention MLWorks and poly 3.x any more, they are untested
2004-04-17, by kleing
add HOL-Matrix
2004-04-17, by kleing
added HOL-Matrix, added HOL/Matrix/ROOT.ML
2004-04-17, by kleing
tuned;
2004-04-16, by wenzelm
more elaborate header markup;
2004-04-16, by wenzelm
tuned document;
2004-04-16, by wenzelm
Pure: 'instance' now handles general arities;
2004-04-16, by wenzelm
'instance' and intro_classes now handle general sorts;
2004-04-16, by wenzelm
exactly1true rewritten (much better when converting to CNF now)
2004-04-16, by webertj
Moved ring stuff from ex into Ring_and_Field.
2004-04-16, by nipkow
Added entry for quickcheck command.
2004-04-16, by berghofe
Replaced quote by Library.quote, since quote now refers to Symbol.quote
2004-04-16, by berghofe
Replaced quote by Pretty.quote / Library.quote, since quote now refers to Symbol.quote
2004-04-16, by berghofe
Replaced quote by Pretty.quote.
2004-04-16, by berghofe
Replaced quote by Library.quote, since quote now refers to Symbol.quote
2004-04-16, by berghofe
Added translate function to String structure.
2004-04-16, by berghofe
- tuned text function
2004-04-16, by berghofe
Added variants of functions quote and commas_quote that allow escaping
2004-04-16, by berghofe
Moved symbol.ML to front of file list (due to quote function).
2004-04-16, by berghofe
first version of matrices for HOL/Isabelle
2004-04-16, by obua
Added theory with examples for quickcheck command.
2004-04-16, by berghofe
lemma drop_Suc_conv_tl added.
2004-04-16, by mehta
simplified ML code for setsubgoaler;
2004-04-16, by wenzelm
tuned document;
2004-04-16, by wenzelm
add locales
2004-04-16, by kleing
Zur Freude von Sebastian Skalberg!
2004-04-16, by ballarin
Added Locales Tutorial.
2004-04-16, by ballarin
say how to install PG and poly
2004-04-16, by kleing
fix cvs id
2004-04-16, by kleing
describe how to work on Isabelle repository version
2004-04-16, by kleing
make weblint happy
2004-04-16, by kleing
updated, tuned
2004-04-16, by kleing
*** empty log message ***
2004-04-16, by nipkow
tuned;
2004-04-16, by wenzelm
session graph;
2004-04-16, by wenzelm
tuned document;
2004-04-16, by wenzelm
add feature list
2004-04-16, by kleing
add faq
2004-04-16, by kleing
add link to FAQ
2004-04-16, by kleing
add Isabelle2003 to archive
2004-04-16, by kleing
tuned;
2004-04-15, by wenzelm
fixed width;
2004-04-15, by wenzelm
finalconsts RepC AbsC;
2004-04-15, by wenzelm
Added ex/Exceptions.thy
2004-04-15, by nipkow
"haspref" -> "oldhaspref" (David Aspinall)
2004-04-15, by nipkow
bugfix in xsymbols_output
2004-04-15, by schirmer
corrected PG url in comment
2004-04-14, by nipkow
use more symbols in HTML output
2004-04-14, by kleing
renamed have_thms to note_thms;
2004-04-14, by wenzelm
tuned;
2004-04-14, by wenzelm
proper handling of lines terminated by CRLF or CR;
2004-04-14, by wenzelm
* raw control symbols are of the form \<^raw:...> now.
2004-04-14, by schirmer
Fixed bug in check_mode_clause.
2004-04-14, by berghofe
bugfix for \<^raw...> scanner
2004-04-14, by schirmer
prod and sum
2004-04-14, by kleing
* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in
2004-04-13, by schirmer
* Calculation commands "moreover" and "also" no longer interfere with
2004-04-13, by wenzelm
'also'/'moreover': do not interfere with current facts, allow in chain mode;
2004-04-13, by wenzelm
export put_thms;
2004-04-13, by wenzelm
Added brief intro text.
2004-04-13, by ballarin
convert symbols to HTML 4.0 character entities,
2004-04-13, by kleing
Various changes to HOL-Algebra;
2004-04-13, by ballarin
hence -> from calculation have
2004-04-13, by kleing
fix moreover/this behaviour:
2004-04-13, by kleing
export thisN
2004-04-13, by kleing
isabelle.css
2004-04-13, by kleing
use .jar
2004-04-13, by kleing
change order of options for jar (fix error on Sun)
2004-04-13, by kleing
ignore GraphBrowser.jar
2004-04-13, by kleing
remove MiniML and Lex (moved to AFP)
2004-04-12, by kleing
use css in generated web pages
2004-04-12, by kleing
use css
2004-04-12, by kleing
use css
2004-04-12, by kleing
produce jar instead of single .class files
2004-04-12, by kleing
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
2004-04-12, by oheimb
added theorem chg_map_other
2004-04-12, by oheimb
added HOLCF/Streams.thy (with concatenation etc.)
2004-04-12, by oheimb
added Streams.thy (with stream concatenation etc.)
2004-04-12, by oheimb
treat sub/super scripts
2004-04-09, by kleing
freeness theorems and induction rule
2004-04-08, by paulson
tidied
2004-04-08, by paulson
new theory
2004-04-08, by paulson
some (much longer) structured proofs
2004-04-08, by paulson
fix time tag of session.tex
2004-04-08, by kleing
Locale instantiation: label parameter optional, new attribute paramter.
2004-04-07, by ballarin
IsaMakefile
2004-04-07, by paulson
new
2004-04-06, by mehta
*** empty log message ***
2004-04-06, by mehta
*** empty log message ***
2004-04-06, by mehta
new
2004-04-06, by streckem
*** empty log message ***
2004-04-06, by mehta
*** empty log message ***
2004-04-06, by mehta
Whoops. Those default cases can be tricky.
2004-04-05, by skalberg