Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-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.
Move some lemmas to List.
2000-01-12, by nipkow
More lemmas.
2000-01-12, by nipkow
isabellesimple: avoid paragraph;
2000-01-10, by wenzelm
int:nat->int is pushed inwards.
2000-01-10, by nipkow
Forgot to "call" MicroJava in makefile.
2000-01-10, by nipkow
tidied parentheses
2000-01-07, by paulson
tidied
2000-01-07, by paulson
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
2000-01-07, by paulson
better automation for "slice"
2000-01-07, by paulson
moved some proofs from UNITY/ELT to UNITY/Project
2000-01-07, by paulson
obtain: renamed 'in' to 'where';
2000-01-06, by wenzelm
oops';
2000-01-05, by wenzelm
oops;
2000-01-05, by wenzelm
improved symbol for subcls relation
2000-01-05, by oheimb
simplified definition of appl_methds, removing m_head
2000-01-05, by oheimb
tuned;
2000-01-05, by wenzelm
obtain;
2000-01-05, by wenzelm
comment: any number of texts;
2000-01-05, by wenzelm
proof markup: any mode;
2000-01-05, by wenzelm
replaced HOLogic.termTVar by HOLogic.termT;
2000-01-05, by wenzelm
ObtainFun;
2000-01-05, by wenzelm
METHOD_CLASET': refer to *local* claset;
2000-01-05, by wenzelm
moved obtain to obtain.ML;
2000-01-05, by wenzelm
TypeInfer.logicT;
2000-01-05, by wenzelm
tuned;
2000-01-05, by wenzelm
ObtainFun;
2000-01-05, by wenzelm
added thms_ctxt_args;
2000-01-05, by wenzelm
prepare patterns only once;
2000-01-05, by wenzelm
ObtainFun;
2000-01-05, by wenzelm
present chapter;
2000-01-05, by wenzelm
removed pats;
2000-01-05, by wenzelm
chapter;
2000-01-05, by wenzelm
support for dummy variables (anyT, logicT);
2000-01-05, by wenzelm
TypeInfer.logicT;
2000-01-05, by wenzelm
new arg type for max_spec etc.
2000-01-04, by oheimb
small changes;
2000-01-03, by bauerg
removed inj_eq from the default simpset again
2000-01-03, by oheimb
removed inj_eq from the default simpset again
2000-01-03, by oheimb
removed inj_eq from the default simpset again
1999-12-23, by oheimb
updated sml package name in installation exmaple
1999-12-23, by kleing
raw_t(e)xt: any proof mode;
1999-12-22, by wenzelm
fixed error msg;
1999-12-22, by wenzelm
marg_comment: repeat;
1999-12-22, by wenzelm
text: string list;
1999-12-22, by wenzelm
tidied, with a bit more progress
1999-12-22, by paulson
Working version after a FAILED attempt to base Follows upon LeadsETo
1999-12-22, by paulson
new weakening laws
1999-12-22, by paulson
removing the "{} : CC" requirement for leadsTo[CC]
1999-12-22, by paulson
back to old sml version (due to c library problems)
1999-12-22, by kleing
some tuning (incorporated David's suggestions)
1999-12-22, by kleing
working with weak LeadsTo in guarantees precondition\!
1999-12-21, by paulson
corrected, improved eMail addresses, user interface section
1999-12-21, by oheimb
now workign as far as System_Alloc_Progress
1999-12-17, by paulson
SOUNDNESS BUG FIX for rotate_rule. The original code did not expect
1999-12-16, by paulson
first working version to Alloc/System_Client_Progress;
1999-12-15, by paulson
expandshort
1999-12-13, by paulson
dist page now in page/dist-{content|layout}
1999-12-09, by kleing
updated;
1999-12-09, by wenzelm
prettyfied
1999-12-09, by kleing
full url to local (munich) page
1999-12-09, by kleing
new web pages integrated
1999-12-09, by kleing
used for new weg page layout
1999-12-09, by kleing
ID line added
1999-12-09, by kleing
new webpage layout
1999-12-09, by kleing
abolition of localTo: instead "guarantees" has local vars as extra argument
1999-12-08, by paulson
used image_eq_UN to speed up slow proofs of base cases
1999-12-08, by paulson
useful lemma eqset_imp_iff
1999-12-08, by paulson
tuned;
1999-12-07, by wenzelm
tuned;
1999-12-07, by wenzelm
added Isar_examples/Fibonacci.thy;
1999-12-07, by wenzelm
Fixed bug in find-functions: list of parameters must be reversed before
1999-12-07, by nipkow
Renamed some vars
1999-12-06, by nipkow
cosmetic mod.
1999-12-02, by nipkow
accommodate current version of rpm;
1999-12-01, by wenzelm
Fixed a problem with returning from the last frame.
1999-12-01, by nipkow
new generalized leads-to theory
1999-12-01, by paulson
fixed the discrepancy in the ordering of the constructors LESS EQUAL GREATER
1999-12-01, by paulson
deleted rogue copy of localTo_imp_o_localTo
1999-11-30, by paulson
working version with new theory ELT
1999-11-30, by paulson
new theory UNITY/ELT
1999-11-30, by paulson
Goal: tuned pris;
1999-11-29, by wenzelm
Removed !!
1999-11-29, by nipkow
Minimal.thy;
1999-11-29, by wenzelm
Isar_examples/Minimal.thy;
1999-11-29, by wenzelm
qed "";
1999-11-29, by wenzelm
Various little changes like cmethd -> method and cfield -> field.
1999-11-26, by nipkow
del Method.ML
1999-11-25, by nipkow
Minor mods.
1999-11-25, by nipkow
renamed comp to compile (avoids clash with Relation.comp);
1999-11-24, by wenzelm
prove_goal thy;
1999-11-24, by wenzelm
Basis now Main.
1999-11-24, by nipkow
tidied, choosing nicer names
1999-11-24, by paulson
distributive laws for * over -
1999-11-23, by paulson
tidied
1999-11-23, by paulson
new theorem rev_image_eqI
1999-11-23, by paulson
Added linord_less_split
1999-11-22, by nipkow
re-shaped and re-ordered conversion relations
1999-11-19, by oheimb
Streamlined it a bit more.
1999-11-18, by nipkow
A small mod.
1999-11-18, by nipkow
added Isar_examples/Puzzle.thy;
1999-11-17, by wenzelm
tidied
1999-11-17, by paulson
Streamlined it a bit.
1999-11-15, by nipkow
removed full_SetCompr_eq from simpset() again
1999-11-12, by oheimb
Added the proof by Nielson & Nielson.
1999-11-12, by nipkow
tuned;
1999-11-12, by wenzelm
HOL changes
1999-11-11, by paulson
*** empty log message ***
1999-11-11, by nipkow
Added MicroJava
1999-11-11, by nipkow
*** empty log message ***
1999-11-11, by nipkow
with_path;
1999-11-11, by wenzelm
Imported Conny's lemmas from MicroJava
1999-11-11, by nipkow
clean target;
1999-11-11, by wenzelm
header;
1999-11-11, by wenzelm
tidied
1999-11-11, by paulson
new-style infix declaration for "image"
1999-11-11, by paulson
Fixed obsolete use of "op ^^"; new lemma
1999-11-11, by paulson
tuned;
1999-11-06, by wenzelm
tidied
1999-11-05, by paulson
new psubset lemma
1999-11-05, by paulson
added foldr
1999-11-05, by paulson
Algebra and Polynomial theories, by Clemens Ballarin
1999-11-05, by paulson
Algebra and Polynomial theories, by Clemens Ballarin
1999-11-05, by paulson
tuned;
1999-11-03, by wenzelm
MUCKE_HOME;
1999-11-03, by wenzelm
Id;
1999-11-03, by wenzelm
improved;
1999-11-03, by wenzelm
tuned;
1999-11-02, by wenzelm
RPMRELEASE;
1999-11-01, by wenzelm
inserted {...}
1999-11-01, by paulson
updated;
Isabelle99
1999-10-31, by wenzelm
updated;
1999-10-31, by wenzelm
tuned;
1999-10-31, by wenzelm
tuned;
1999-10-31, by wenzelm
Isabelle99;
1999-10-30, by wenzelm
fixed deps;
1999-10-30, by wenzelm
tuned;
1999-10-30, by wenzelm
tuned;
1999-10-30, by wenzelm
improved presentation;
1999-10-30, by wenzelm
tuned;
1999-10-30, by wenzelm
isabellesym.sty;
1999-10-30, by wenzelm
definitions of many Isabelle symbols;
1999-10-30, by wenzelm
final update by Gertrud Bauer;
1999-10-29, by wenzelm
workaround bug (feature?) in bibtex;
1999-10-29, by wenzelm
tuned;
1999-10-29, by wenzelm
comment out isabellesym.sty;
1999-10-29, by wenzelm
improved;
1999-10-29, by wenzelm
\isasymbol renamed to \isasym;
1999-10-29, by wenzelm
tuned;
1999-10-29, by wenzelm
tuned msg;
1999-10-29, by wenzelm
\isasym;
1999-10-29, by wenzelm
improved singleton_insert_inj_eq
1999-10-29, by oheimb
improved presentation;
1999-10-28, by wenzelm
fixed deps;
1999-10-28, by wenzelm
tuned;
1999-10-28, by wenzelm
expandshort; tidied
1999-10-28, by paulson
localTo_imp_o_localTo is now really an implication
1999-10-28, by paulson
simplified the stable_completion proofs
1999-10-28, by paulson
tidied
1999-10-28, by paulson
expandshort
1999-10-28, by paulson
improved IsarThy.init_context;
1999-10-28, by wenzelm
tuned;
1999-10-28, by wenzelm
added various little lemmas
1999-10-27, by oheimb
clarsimp_tac now copes with the (unwanted) case that the simplifier splits
1999-10-27, by oheimb
tuned msg;
1999-10-27, by wenzelm
tuned;
1999-10-27, by wenzelm
added (try_)update_thy_only;
1999-10-27, by wenzelm
added init_context;
1999-10-27, by wenzelm
quiet_update_thy: ml flag;
1999-10-27, by wenzelm
Fixed a bug in the EX simproc.
1999-10-27, by nipkow
export cond_with_path;
1999-10-27, by wenzelm
dummy_pattern: aprop;
1999-10-27, by wenzelm
updated for Isabelle99;
1999-10-27, by wenzelm
working again; new treatment of LocalTo
1999-10-27, by paulson
TEMPORARY use of Addsimps
1999-10-27, by paulson
got rid of split_diff, which duplicated nat_diff_split, and
1999-10-27, by paulson
symbols in (error) messages now consistently with single backslash
1999-10-27, by oheimb
now more than 256 generated bound variables possible
1999-10-27, by oheimb
reset_goals no longer empties the proof stack
1999-10-27, by oheimb
improved ml handling;
1999-10-26, by wenzelm
improved ml handling;
1999-10-26, by wenzelm
tuned;
1999-10-26, by wenzelm
activate ml_prompts;
1999-10-26, by wenzelm
added inform_file_processed, inform_file_retracted;
1999-10-26, by wenzelm
added kill_proof_notify;
1999-10-26, by wenzelm
added check_known_thy, if_known_thy;
1999-10-26, by wenzelm
Isabelle %f;
1999-10-26, by wenzelm
do not set proof_timing;
1999-10-26, by wenzelm
export kill_theory;
1999-10-26, by wenzelm
added kill_thy;
1999-10-26, by wenzelm
added opt_unit (from isar_syn.ML);
1999-10-26, by wenzelm
added drop_ext;
1999-10-26, by wenzelm
improved handling of warn_extra_tfrees;
1999-10-25, by wenzelm
update by Gertrud Bauer;
1999-10-25, by wenzelm
added Real/HahnBanach/document/root.bib;
1999-10-25, by wenzelm
warn_extra_tfrees (after declare_term);
1999-10-22, by wenzelm
warn_extra_tfrees;
1999-10-22, by wenzelm
warn_extra_tfrees;
1999-10-22, by wenzelm
tuned repeat_undo;
1999-10-22, by wenzelm
debug_simp;
1999-10-22, by wenzelm
new flag debug_simp
1999-10-22, by wenzelm
tuned simplifier trace output; new flag debug_simp
1999-10-22, by wenzelm
achieve proper italic correction;
1999-10-22, by wenzelm
HahnBanach update by Gertrud Bauer;
1999-10-22, by wenzelm
replaced image_image_eq_UN by image_eq_UN
1999-10-22, by paulson
ALMOST working version: LocalTo results commented out
1999-10-22, by paulson
new default simprules for UN and INT
1999-10-22, by paulson
new theorems on Image
1999-10-22, by paulson
tidied using modern infix form
1999-10-22, by paulson
tuned trace_action;
1999-10-21, by wenzelm
added known_thy;
1999-10-21, by wenzelm
end/kill_theory: check_known_thy;
1999-10-21, by wenzelm
added touch_child_thys;
1999-10-21, by wenzelm
\isakeyword: fixed italic correction;
1999-10-21, by wenzelm
get_thm;
1999-10-21, by wenzelm
tuned;
1999-10-21, by wenzelm
proper handling of axioms / defs;
1999-10-21, by wenzelm
markup: keep indentation;
1999-10-21, by wenzelm
added is_indent;
1999-10-21, by wenzelm
export thy_path;
1999-10-21, by wenzelm
output \isasymbols;
1999-10-21, by wenzelm
forall_elim_var(s) move here from drule.ML;
1999-10-21, by wenzelm
forall_elim_var(s) moved to pure_thy.ML;
1999-10-21, by wenzelm
*** empty log message ***
1999-10-21, by wenzelm
removed \BG, \EN;
1999-10-21, by wenzelm
updated;
1999-10-21, by wenzelm
added \ISS;
1999-10-21, by wenzelm
eliminated isar_action;
1999-10-20, by wenzelm
remove_thy: warn unknown theory (rather than error);
1999-10-20, by wenzelm
use_mltext: better control of verbosity;
1999-10-20, by wenzelm
use_text: remove last char from output;
1999-10-20, by wenzelm
option -m TARGET;
1999-10-20, by wenzelm
removed -B option;
1999-10-20, by wenzelm
tuned usage;
1999-10-20, by wenzelm
the settings environment is now statically scoped;
1999-10-20, by wenzelm
fixed update_thy_only;
1999-10-20, by wenzelm
qed_spec_mp is a mess;
1999-10-19, by wenzelm
tuned;
1999-10-19, by wenzelm
tuned;
1999-10-18, by wenzelm
update by Stephan Merz;
1999-10-18, by wenzelm
exchanged the first two args of "project" and "drop_prog"
1999-10-18, by paulson
fixed comments
1999-10-18, by paulson
working version with localTo[C] instead of localTo
1999-10-18, by paulson
new thm disjoint_iff_not_equal
1999-10-18, by paulson
new thm vimage_image_eq
1999-10-18, by paulson
PROOFGENERAL_OPTIONS="-u false";
1999-10-16, by wenzelm
improved presentation;
1999-10-15, by wenzelm
fixed comment;
1999-10-15, by wenzelm
Removed obsolete comment.
1999-10-15, by berghofe
Documented thm_deps.
1999-10-15, by berghofe
Corrected typo.
1999-10-14, by berghofe
improved presentation;
1999-10-14, by wenzelm
support thumbpdf;
1999-10-14, by wenzelm
fixed comment;
1999-10-14, by wenzelm
pdf: generate thumbnails if ISABELLE_THUMBPDF set;
1999-10-14, by wenzelm
support thumbpdf (via 'png' output format);
1999-10-14, by wenzelm
thumbpdf (disabled by default);
1999-10-14, by wenzelm
document preparation based on (PDF)LaTeX;
1999-10-14, by wenzelm
renamed verbatim/verb to text_raw/txt_raw;
1999-10-14, by wenzelm
tuned;
1999-10-14, by wenzelm
improved presentation;
1999-10-14, by wenzelm
berghofe;
1999-10-13, by wenzelm
isabelle-isar-ref;
1999-10-13, by wenzelm
tuned usage;
1999-10-13, by wenzelm
-d pdf;
1999-10-13, by wenzelm
system;
1999-10-13, by wenzelm
use_text_verbose;
1999-10-13, by wenzelm
system;
1999-10-13, by wenzelm
markup / varbatim: comment out (%) newline char;
1999-10-13, by wenzelm
use_text writeln;
1999-10-13, by wenzelm
mkdir, copy_all: system_command;
1999-10-13, by wenzelm
updated;
1999-10-13, by wenzelm
Eliminated mutual_induct_tac.
1999-10-13, by berghofe
Eliminated mutual_induct_tac.
1999-10-13, by berghofe
Eliminated mutual_induct_tac.
1999-10-13, by berghofe
more Collect laws
1999-10-13, by paulson
deleted the redundant less_imp_binomial_eq_0
1999-10-13, by paulson
choose just as an infix
1999-10-13, by paulson
simplified and generalized n_sub_lemma and n_subsets
1999-10-13, by paulson
working snapshot; more steps in Alloc
1999-10-13, by paulson
projecting/extending version of drop_prog_guarantees
1999-10-13, by paulson
new theorem set_mono
1999-10-13, by paulson
a4paper;
1999-10-12, by wenzelm
a4paper;
1999-10-12, by wenzelm
a4paper;
1999-10-12, by wenzelm
a4paper;
1999-10-12, by wenzelm
new "choose" lemmas by Florian Kammueller
1999-10-12, by paulson
improved presentation;
1999-10-11, by wenzelm
bind_thm "ccontr";
1999-10-11, by wenzelm
files: separate by " ";
1999-10-11, by wenzelm
- Documented monotonicity theorems.
1999-10-11, by berghofe
a4paper;
1999-10-11, by wenzelm
tuned packages;
1999-10-11, by wenzelm
a4paper;
1999-10-11, by wenzelm
working shapshot with "projecting" and "extending"
1999-10-11, by paulson
replaced {x. True} by UNIV to work with the new simprule, Collect_const
1999-10-11, by paulson
new default simprule Collect_const and new them Diff_insert_absorb
1999-10-11, by paulson
new thm vimage_INT; deleted redundant UN_vimage
1999-10-11, by paulson
new thm Domain_mono
1999-10-11, by paulson
new thm card_Diff_singleton; tidied
1999-10-11, by paulson
more explanations;
1999-10-09, by wenzelm
tuned presentation;
1999-10-09, by wenzelm
added structured version of the proof;
1999-10-09, by wenzelm
improved;
1999-10-09, by wenzelm
bib;
1999-10-09, by wenzelm
support bibtex;
1999-10-09, by wenzelm
check format;
1999-10-09, by wenzelm
added ISABELLE_BIBTEX;
1999-10-09, by wenzelm
removed 8bit;
1999-10-09, by wenzelm
\isakeyword: italic correction;
1999-10-08, by wenzelm
old_header: proper error message;
1999-10-08, by wenzelm
tuned presentation;
1999-10-08, by wenzelm
update from Gertrud;
1999-10-08, by wenzelm
tuned;
1999-10-08, by wenzelm
url;
1999-10-08, by wenzelm
theorem database now also indexes constants "Trueprop", "all",
1999-10-08, by wenzelm
improved;
1999-10-08, by wenzelm
removed generated index.html;
1999-10-08, by wenzelm
isatool_document;
1999-10-08, by wenzelm
make: tuned usage;
1999-10-08, by wenzelm
improved presentation;
1999-10-08, by wenzelm
include document;
1999-10-08, by wenzelm
return stored thms with proper naming in derivation;
1999-10-08, by wenzelm
improved special chars;
1999-10-08, by wenzelm
removed -c option;
1999-10-08, by wenzelm
tuned usage;
1999-10-08, by wenzelm
pass RC;
1999-10-08, by wenzelm
prepare theory session document;
1999-10-08, by wenzelm
*** empty log message ***
1999-10-08, by wenzelm
tuned;
1999-10-08, by wenzelm
cd: quiet;
1999-10-07, by wenzelm
verbatim markup tokens;
1999-10-07, by wenzelm
removed verbatim markups;
1999-10-07, by wenzelm
unset ISABELLE_SETTINGS_PRESENT;
1999-10-07, by wenzelm
Replaced update_new by update.
1999-10-07, by berghofe
Added functions for enabling and disabling derivations.
1999-10-07, by berghofe
read_idents;
1999-10-07, by wenzelm
$ISATOOL;
1999-10-07, by wenzelm
unset ISABELLE_SETTINGS_PRESENT;
1999-10-07, by wenzelm
delete Tools;
1999-10-07, by wenzelm
Documented changes to HOL/inductive and function thm_deps.
1999-10-07, by berghofe
Added file Thy/thm_deps.ML
1999-10-07, by berghofe
obsolete;
1999-10-07, by wenzelm
tuned dirname;
1999-10-07, by wenzelm
removed TeX environment hacking;
1999-10-07, by wenzelm
verbatim / verb markupup commands;
1999-10-07, by wenzelm
Present.token_source after load (better errors!?);
1999-10-07, by wenzelm
Document preparation setup;
1999-10-07, by wenzelm
Isabelle wrapper for LaTeX (and friends);
1999-10-07, by wenzelm
verbatim: no markup;
1999-10-07, by wenzelm
ISABELLE_SETTINGS_PRESENT: avoid multiple invocation;
1999-10-07, by wenzelm
tex_source: Buffer.write;
1999-10-07, by wenzelm
present source *before* theory load;
1999-10-07, by wenzelm
removed write_nonempty;
1999-10-07, by wenzelm
New option -d for deleting file after use.
1999-10-07, by berghofe
New function thm_deps for visualizing dependencies of theorems.
1999-10-07, by berghofe
Added file thm_deps.
1999-10-07, by berghofe
Exported function get_info.
1999-10-07, by berghofe
ISABELLE_USEDIR_OPTIONS: -d pdf option (off by default);
1999-10-06, by wenzelm
improved presentation;
1999-10-06, by wenzelm
Isar_examples/W_correct;
1999-10-06, by wenzelm
tuned presentation;
1999-10-06, by wenzelm
tuned markup commands;
1999-10-06, by wenzelm
Latex.token;
1999-10-06, by wenzelm
improved presentation;
1999-10-06, by wenzelm
improved present_token;
1999-10-06, by wenzelm
added write_nonempty;
1999-10-06, by wenzelm
fixed naming of single axioms;
1999-10-06, by wenzelm
accomodate markup commands;
1999-10-06, by wenzelm
tuned comment;
1999-10-06, by wenzelm
added markup_command;
1999-10-06, by wenzelm
OuterSyntax.markup_command;
1999-10-06, by wenzelm
improved presentation;
1999-10-06, by wenzelm
added document;
1999-10-05, by wenzelm
simplified;
1999-10-05, by wenzelm
strip_blanks;
1999-10-05, by wenzelm
got rid of most;
1999-10-05, by wenzelm
rep_datatype now stores theorems properly.
1999-10-05, by berghofe
fixed title;
1999-10-05, by wenzelm
added document;
1999-10-05, by wenzelm
tuned comments;
1999-10-05, by wenzelm
tuned comment;
1999-10-05, by wenzelm
fixed ml_store_thm(s): deriv;
1999-10-05, by wenzelm
document preparation options: -c -d;
1999-10-05, by wenzelm
conditional url/hyperref setup;
1999-10-05, by wenzelm
present token source;
1999-10-05, by wenzelm
replace add_title by add_header;
1999-10-05, by wenzelm
clear_undo replaced by clear_undos;
1999-10-05, by wenzelm
added is_toplevel;
1999-10-05, by wenzelm
clear: int argument;
1999-10-05, by wenzelm
use_dir: doc;
1999-10-05, by wenzelm
replaced clear_undo by clear_undos;
1999-10-05, by wenzelm
outer_lex.ML loaded in Thy;
1999-10-05, by wenzelm
include browser_info stuff;
1999-10-05, by wenzelm
Simple LaTeX presentation primitives (based on outer lexical syntax).
1999-10-05, by wenzelm
begin_index: document;
1999-10-05, by wenzelm
moved stuff to present.ML;
1999-10-05, by wenzelm
added Thy/latex.ML;
1999-10-05, by wenzelm
Got rid of readtm.
1999-10-05, by berghofe
Tuned inductive definition.
1999-10-05, by berghofe
updated;
1999-10-05, by wenzelm
added Thy/latex.ML;
1999-10-05, by wenzelm
Present.setup;
1999-10-05, by wenzelm
Added attribute rulify_prems (useful for modifying premises of introduction
1999-10-05, by berghofe
added copy_all;
1999-10-05, by wenzelm
clear: int arg;
1999-10-05, by wenzelm
added position;
1999-10-05, by wenzelm
Additional rules for inductive package.
1999-10-05, by berghofe
added untabify;
1999-10-05, by wenzelm
Rule not_not is now stored in theory (needed by Inductive).
1999-10-05, by berghofe
Monotonicity rules for inductive definitions can now be added to a theory via
1999-10-05, by berghofe
macros for Isabelle generated LaTeX output;
1999-10-05, by wenzelm
arithmetic now in IntArith;
1999-10-04, by wenzelm
simprocs now in IntArith;
1999-10-04, by wenzelm
IntArith;
1999-10-04, by wenzelm
Tools/typedef_package.ML;
1999-10-04, by wenzelm
eliminated ap/app;
1999-10-04, by wenzelm
proper dependencies of all theories and packages;
1999-10-04, by wenzelm
removed DatatypePackage.setup;
1999-10-04, by wenzelm
load / setup recdef package (TFL);
1999-10-04, by wenzelm
load / setup datatype package;
1999-10-04, by wenzelm
removed TFL/sys.sml;
1999-10-04, by wenzelm
obsolete;
1999-10-04, by wenzelm
renamed 'prefix' to 'prfx' (avoids clash with infix);
1999-10-04, by wenzelm
tuned;
1999-10-04, by wenzelm
mk_frees, assume_read moved here;
1999-10-04, by wenzelm
tryres, gen_make_elim moved here;
1999-10-04, by wenzelm
FOLogic.mk_conj;
1999-10-04, by wenzelm
added mk_conj, mk_disj, mk_imp;
1999-10-04, by wenzelm
added BVC;
1999-10-04, by wenzelm
added mk_conj, mk_disj, mk_imp;
1999-10-04, by wenzelm
working snapshot (even Alloc)
1999-10-04, by paulson
most results now refer to those for "extend"
1999-10-04, by paulson
fixed lookup_theory;
1999-10-04, by wenzelm
fixed CHANGED_GOAL, which is used by stac
1999-10-04, by paulson
improved theory_source presentation (hook);
1999-10-03, by wenzelm
improved theory_source presentation;
1999-10-03, by wenzelm
export token_source;
1999-10-03, by wenzelm
added Space, Comment token kinds (keep actual text);
1999-10-03, by wenzelm
fixed no_qed;
1999-10-01, by wenzelm
added Isar/obtain.ML;
1999-10-01, by wenzelm
improved 'fix' / Skolem interfaces;
1999-10-01, by wenzelm
added 'obtain' command;
1999-10-01, by wenzelm
tuned comment;
1999-10-01, by wenzelm
added prf_asm_goal;
1999-10-01, by wenzelm
added atomic_thesis;
1999-10-01, by wenzelm
The 'obtain' language element -- achieves (eliminated) existential
1999-10-01, by wenzelm
added undef_global_attribute, undef_local_attribute;
1999-10-01, by wenzelm
- Fixed bug in mk_split_pack which caused application of expansion theorem
1999-10-01, by berghofe
fixed 'is' match;
1999-09-30, by wenzelm
added cert_skolem;
1999-09-30, by wenzelm
export find_free;
1999-09-30, by wenzelm
removed ProofContext.declare_thm;
1999-09-30, by wenzelm
local_def_i: typ option;
1999-09-30, by wenzelm
fix_i, local_def_i: typ option;
1999-09-30, by wenzelm
get_goal: prop;
1999-09-30, by wenzelm
insert: ignore facts;
1999-09-30, by wenzelm
export def_sort, def_type;
1999-09-30, by wenzelm
Real/HahnBanach;
1999-09-30, by wenzelm
depend on Main;
1999-09-30, by wenzelm
now with (weak safety) guarantees (weak progress) with Extend
1999-09-30, by paulson
bind_thm ("case_split", case_split_thm);
1999-09-29, by wenzelm
CollectE;
1999-09-29, by wenzelm
subsetD;
1999-09-29, by wenzelm
update from Gertrud;
1999-09-29, by wenzelm
The Hahn-Banach theorem for real vectorspaces;
1999-09-29, by wenzelm
bind_thms;
1999-09-29, by wenzelm
Sign.defaultS;
1999-09-29, by wenzelm
Sign.of_sort;
1999-09-29, by wenzelm
tuned;
1999-09-29, by wenzelm
removed force_strip_shyps;
1999-09-29, by wenzelm
lemma;
1999-09-29, by wenzelm
bind_thms;
1999-09-29, by wenzelm
proper handling of dangling sort hypotheses (at last!);
1999-09-29, by wenzelm
mk_simps: do *not* include Thm.strip_shyps o Drule.zero_var_indexes
1999-09-29, by wenzelm
Sign.defaultS;
1999-09-29, by wenzelm
strip_shyps(_warning);
1999-09-29, by wenzelm
mg_domain: exception DOMAIN;
1999-09-29, by wenzelm
removed implies_intr_shyps;
1999-09-29, by wenzelm
added witness_sorts, univ_witness;
1999-09-29, by wenzelm
added witness_sorts, univ_witness;
1999-09-29, by wenzelm
less
more
|
(0)
-3000
-1000
-480
+480
+1000
+3000
+10000
+30000
tip