Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-512
+512
+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.
split_conv;
2001-01-16, by wenzelm
updated;
2001-01-16, by wenzelm
isabelle -f;
2001-01-16, by wenzelm
more method_setup examples;
2001-01-16, by wenzelm
lcp's pass over the book, chapters 1-8
2001-01-15, by paulson
removed instructions Aconst_null+Bipush, introduced LitPush
2001-01-14, by kleing
tuned
2001-01-14, by kleing
*** empty log message ***
2001-01-14, by nipkow
use_text_verbose: priority output;
2001-01-12, by wenzelm
use_mltext: priority output;
2001-01-12, by wenzelm
HOLogic.dest_binum;
2001-01-12, by wenzelm
hide dest_bin;
2001-01-12, by wenzelm
HOLogic.dest_binum;
2001-01-12, by wenzelm
wrong font for braces
2001-01-12, by paulson
LateX-2e moans about using \\choose
2001-01-12, by paulson
the \\epsilon character causes font errors in a section title
2001-01-12, by paulson
made SML/NJ happy;
2001-01-12, by wenzelm
lcp's pass over the book, chapters 1-8
2001-01-12, by paulson
renaming of some files
2001-01-12, by paulson
updated for new version of even-examples.tex
2001-01-12, by paulson
updated for new version of advanced-examples.tex
2001-01-12, by paulson
abs and other small changes
2001-01-12, by paulson
updated for new version of numerics.tex
2001-01-12, by paulson
renaming to avoid clashes
2001-01-12, by paulson
auto update
2001-01-12, by paulson
general revisions
2001-01-12, by paulson
added Sigma_Algebra;
2001-01-12, by wenzelm
added Induct/Sigma_Algebra.thy;
2001-01-12, by wenzelm
tuned;
2001-01-12, by wenzelm
do not hilite "xnum";
2001-01-11, by wenzelm
make_raw: do not AutoBind.drop_judgment;
2001-01-11, by wenzelm
induct cases: RuleCases.make_raw;
2001-01-11, by wenzelm
added strict_prefixI', strict_prefixE';
2001-01-11, by wenzelm
subst syntax;
2001-01-11, by wenzelm
*** empty log message ***
2001-01-11, by nipkow
lcp's suggestions for CTL
2001-01-11, by paulson
*** empty log message ***
2001-01-11, by nipkow
a new label
2001-01-11, by paulson
revisions corresponding to the new version of sets.tex
2001-01-11, by paulson
Added <cdot> syntax for continuous application $.
2001-01-10, by nipkow
isatool unsymbolize;
2001-01-10, by wenzelm
updated;
2001-01-10, by wenzelm
tuned \DOT, \DDOT;
2001-01-10, by wenzelm
added \<wrong> symbol;
2001-01-10, by wenzelm
tuned;
2001-01-10, by wenzelm
revisions e.g. images, transitive closure...
2001-01-10, by paulson
*** empty log message ***
2001-01-10, by nipkow
*** empty log message ***
2001-01-10, by nipkow
case_tac on bools
2001-01-10, by paulson
case_tac subgoals
2001-01-10, by paulson
deleted the obsolete nat_neqE (and reformatting)
2001-01-10, by paulson
deleted the obsolete nat_neqE
2001-01-10, by paulson
generalizing the LEAST theorems from "nat" to linear
2001-01-10, by paulson
now using "by" for one-line proofs
2001-01-10, by paulson
various changes including the SOME examples, rule_format and "by"
2001-01-10, by paulson
loads the new theory
2001-01-10, by paulson
reformatting, and splitting the end of "Primes" to create "Forward"
2001-01-10, by paulson
*** empty log message ***
2001-01-10, by nipkow
now using "by" for one-line proofs
2001-01-10, by paulson
introduction of "by" and a few examples of SOME
2001-01-10, by paulson
auto update
2001-01-10, by paulson
new wfrec example
2001-01-10, by paulson
fixed the treatment of Rules and Sets
2001-01-10, by paulson
*** empty log message ***
2001-01-10, by nipkow
use \<acute>;
2001-01-10, by wenzelm
added \<dieresis>, \<acute>, \<cedilla>, \<emptyset>;
2001-01-10, by wenzelm
added acute, cedilla, dieresis, hungarumlaut;
2001-01-09, by wenzelm
` -> $
2001-01-09, by nipkow
*** empty log message ***
2001-01-09, by nipkow
`` -> ` and ``` -> ``
2001-01-09, by nipkow
`` -> and ``` -> ``
2001-01-09, by nipkow
replaced \<macron> by \<inverse>;
2001-01-09, by wenzelm
avoid renaming of params in cases;
2001-01-09, by wenzelm
split_all operation;
2001-01-09, by wenzelm
improved evaluation judgment syntax; modified Loop rule
2001-01-09, by oheimb
syntax (xsymbols);
2001-01-09, by wenzelm
Removed Applyall
2001-01-08, by nipkow
additional pattern allows reduction of fractions to lowest terms
2001-01-08, by paulson
*** empty log message ***
2001-01-08, by nipkow
updated;
2001-01-07, by wenzelm
removed ID (avoid CVS conflicts with generated versions);
2001-01-07, by wenzelm
CHANGED_PROP;
2001-01-07, by wenzelm
removed MicroJava/BV/Convert.thy;
2001-01-07, by wenzelm
do not AutoBind.drop_judgment;
2001-01-07, by wenzelm
tuned output;
2001-01-07, by wenzelm
tuned norm_hhf(_tac);
2001-01-07, by wenzelm
added is_norm_hhf;
2001-01-07, by wenzelm
removed outdated comment;
2001-01-07, by wenzelm
case binds: AutoBind.drop_judgment;
2001-01-07, by wenzelm
tuned split_all_tac;
2001-01-07, by wenzelm
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
2001-01-07, by kleing
support ?case binding;
2001-01-06, by wenzelm
apply_case: more robust handling of bounds;
2001-01-06, by wenzelm
moved norm_hhf_tac to Pure/tactic.ML;
2001-01-06, by wenzelm
added drop_judgment;
2001-01-06, by wenzelm
export read_inst', inst';
2001-01-06, by wenzelm
added list_abs;
2001-01-06, by wenzelm
added norm_hhf(_tac);
2001-01-06, by wenzelm
Tactic.norm_hhf;
2001-01-06, by wenzelm
'of:' params spec;
2001-01-06, by wenzelm
'cases' / 'induct' method: ?case binding, 'of:' spec;
2001-01-06, by wenzelm
*** empty log message ***
2001-01-06, by nipkow
*** empty log message ***
2001-01-06, by nipkow
*** empty log message ***
2001-01-06, by nipkow
*** empty log message ***
2001-01-05, by nipkow
^^ -> ```
2001-01-05, by nipkow
Fleuriot reference
2001-01-05, by paulson
minor edits to Chapters 1-3
2001-01-05, by paulson
revisions especially concerning the reals
2001-01-05, by paulson
*** empty log message ***
2001-01-05, by nipkow
a few extra brackets
2001-01-05, by paulson
*** empty log message ***
2001-01-05, by nipkow
*** empty log message ***
2001-01-05, by nipkow
Changed priority of dvd from 70 to 50 as befits a relation.
2001-01-05, by nipkow
*** empty log message ***
2001-01-05, by nipkow
new UNITY examples by Sidi Ehmety
2001-01-05, by paulson
Field of a relation, and some Domain/Range rules
2001-01-05, by paulson
finite_trancl: new theorem by Sidi Ehmety
2001-01-05, by paulson
more removal of obsolete rules
2001-01-05, by paulson
fixed two proofs that were affected by the removal of obsolete rules
2001-01-05, by paulson
new examples by Sidi Ehmety
2001-01-05, by paulson
tuned comment;
2001-01-04, by wenzelm
renamed .sml files to .ML;
2001-01-04, by wenzelm
label!
2001-01-04, by nipkow
more tidying, especially to remove real_of_posnat
2001-01-04, by paulson
initial material on the Reals
2001-01-04, by paulson
updated;
2001-01-03, by wenzelm
added recdef_tc(_i);
2001-01-03, by wenzelm
recdef_tc;
2001-01-03, by wenzelm
renamed .sml files to .ML;
2001-01-03, by wenzelm
TFL: renamed .sml to .ML;
2001-01-03, by wenzelm
added 'recdef_tc' command;
2001-01-03, by wenzelm
* Isar/HOL: added 'recdef_tc' command;
2001-01-03, by wenzelm
renamed .sml files to .ML;
2001-01-03, by wenzelm
tuned;
2001-01-03, by wenzelm
Thm: dest_comb, dest_abs, capply, cabs no longer global;
2001-01-03, by wenzelm
removal of the nat_cancel_factor simproc
2001-01-03, by paulson
Types chapter now uses HOL-Real
2001-01-03, by paulson
some HOL-Real material
2001-01-03, by paulson
added type annotation to Call
2001-01-02, by oheimb
*** empty log message ***
2001-01-02, by nipkow
*** empty log message ***
2001-01-02, by nipkow
*** empty log message ***
2001-01-02, by nipkow
*** empty log message ***
2001-01-02, by nipkow
minor tidying of simprocs
2001-01-01, by paulson
put in some missing Hyperreal files
2001-01-01, by paulson
Hyperreal
2001-01-01, by paulson
separation of HOL-Hyperreal from HOL-Real
2000-12-31, by paulson
now #16*(x+y) distributes for nat just as for other numeric types
2000-12-30, by paulson
a generic ordering theorem used in Real
2000-12-30, by paulson
tidying, and separation of HOL-Hyperreal from HOL-Real
2000-12-30, by paulson
separation of HOL-Hyperreal from HOL-Real
2000-12-30, by paulson
separation of HOL-Hyperreal from HOL-Real
2000-12-30, by paulson
recover: ignore result;
2000-12-29, by wenzelm
recover: malformed result;
2000-12-29, by wenzelm
scan: malformed result;
2000-12-29, by wenzelm
recover: result;
2000-12-29, by wenzelm
proper error msg;
2000-12-29, by wenzelm
'erule' etc.: assm arg;
2000-12-27, by wenzelm
Method.erule 0;
2000-12-27, by wenzelm
updated;
2000-12-27, by wenzelm
'insert' made proper;
2000-12-27, by wenzelm
ares_tac, [edf]atac;
2000-12-27, by wenzelm
antiq: preview errors;
2000-12-23, by wenzelm
tuned length;
2000-12-23, by wenzelm
tuned output;
2000-12-23, by wenzelm
recover_order for single step tules;
2000-12-23, by wenzelm
simplified quick_and_dirty stuff;
2000-12-23, by wenzelm
tuned;
2000-12-23, by wenzelm
hide type node item;
2000-12-23, by wenzelm
Tools/string_syntax.ML;
2000-12-23, by wenzelm
tuned comment;
2000-12-23, by wenzelm
SML90 stuff;
2000-12-22, by wenzelm
handle proper rules;
2000-12-22, by wenzelm
export rewrite_cterm;
2000-12-22, by wenzelm
added inductive_conj;
2000-12-22, by wenzelm
tuned;
2000-12-22, by wenzelm
better definitions of SML90 features
2000-12-22, by paulson
*** empty log message ***
2000-12-21, by nipkow
something stopped working, had to add real_add_ac
2000-12-21, by nipkow
rational linear arithmetic
2000-12-21, by nipkow
this makes the proof run (or run faster)
2000-12-21, by paulson
further tidying of NSA proofs
2000-12-21, by paulson
*** empty log message ***
2000-12-21, by nipkow
rational arithmetic
2000-12-21, by nipkow
rational arithemtic
2000-12-21, by nipkow
re-orientation of integer literals
2000-12-21, by paulson
more tidying, especially to rationalize the simprules
2000-12-21, by paulson
re-orientation of 0=... (no idea why the backslashes have changed too)
2000-12-21, by paulson
simproc bug fix: negative literals and large terms
2000-12-21, by paulson
further tidying
2000-12-20, by paulson
generalized the re-orientation 0f 0=... to all types
2000-12-20, by paulson
tidying, removing obsolete lemmas about 0=... and 1=...
2000-12-20, by paulson
tidying, removing obsolete lemmas about 0=...
2000-12-20, by paulson
SML90: ord, chr, explode, implode;
2000-12-20, by wenzelm
re-orienting equations with #nnn on the lhs
2000-12-19, by paulson
re-orienting equations with 0, 1, 2 on the lhs
2000-12-19, by paulson
new file extract_common_term.ML for the cancel-factor simprocs
2000-12-19, by paulson
inserting the simproc nat_cancel_factor
2000-12-19, by paulson
inserting the simproc int_cancel_factor
2000-12-19, by paulson
new simprule zero_less_abs_iff
2000-12-19, by paulson
coping with the re-orientation of #nn=x
2000-12-19, by paulson
cancel-factor simproc allows shorter proofs
2000-12-19, by paulson
more tidying
2000-12-19, by paulson
cancel-factor simproc allows a shorter proof
2000-12-19, by paulson
improved errors;
2000-12-19, by wenzelm
*** empty log message ***
2000-12-18, by nipkow
*** empty log message ***
2000-12-18, by nipkow
new simproc for cancelling common factors, etc.
2000-12-18, by paulson
moved mk_bin from Numerals to HOLogic
2000-12-18, by nipkow
added rational arithmetic
2000-12-18, by nipkow
towards rtional arithmetic
2000-12-18, by nipkow
tidying and adding new proofs
2000-12-18, by paulson
loads the new simproc extract_common_term
2000-12-18, by paulson
'def': \<equiv>;
2000-12-16, by wenzelm
tuned HOL/Real/HahnBanach;
2000-12-16, by wenzelm
'def': equiv;
2000-12-16, by wenzelm
\isasymequiv;
2000-12-16, by wenzelm
updated;
2000-12-15, by wenzelm
corrected errors;
2000-12-15, by bauerg
usedir -m brackets;
2000-12-15, by wenzelm
GPLed;
2000-12-15, by wenzelm
tuned comment;
2000-12-15, by wenzelm
restore \int (integral);
2000-12-15, by wenzelm
tuned symbols;
2000-12-15, by wenzelm
further round of tidying
2000-12-15, by paulson
*** empty log message ***
2000-12-15, by nipkow
'typedef': present result theorem "type_definition Rep Abs A";
2000-12-14, by wenzelm
tuned;
2000-12-14, by wenzelm
unsymbolize;
2000-12-14, by wenzelm
use \<Sum> from main HOL;
2000-12-14, by wenzelm
added Summation;
2000-12-14, by wenzelm
many new proofs; still needs tidying
2000-12-14, by paulson
new theorem real_lbound_gt_zero
2000-12-14, by paulson
updated;
2000-12-13, by wenzelm
eliminated GOAL syntax;
2000-12-13, by wenzelm
fixed add_term_names: NameSpace.base;
2000-12-13, by wenzelm
tuned comments;
2000-12-13, by wenzelm
* print modes "brackets" and "no_brackets" control output of nested =>
2000-12-13, by wenzelm
tidying
2000-12-13, by paulson
new material, including default simprules that should be introduced earlier
2000-12-13, by paulson
fixed iter_wf proof
2000-12-13, by kleing
another round of tidying-up
2000-12-13, by paulson
working proofs up to isCont_has_Ub
2000-12-13, by paulson
tidying and replacement of "integer" rules by "order" ones
2000-12-13, by paulson
removed sorry proof
2000-12-13, by kleing
tries harder to remove negative literals, e.g.
2000-12-13, by paulson
*** empty log message ***
2000-12-13, by nipkow
*** empty log message ***
2000-12-13, by nipkow
small mods.
2000-12-13, by nipkow
sar split method uses new gen_split_tac.
2000-12-13, by nipkow
completeness (unfinished)
2000-12-12, by kleing
added direction dynamic ==> static
2000-12-12, by kleing
eliminated some warnings, tuned
2000-12-12, by kleing
first stage in tidying up Real and Hyperreal.
2000-12-12, by paulson
deleting unused rules
2000-12-12, by paulson
greater use of overloaded rules (order_less_imp_le not zless_imp_zle, ...)
2000-12-12, by paulson
auto-updated
2000-12-12, by paulson
"translations": allow harpoons;
2000-12-11, by wenzelm
moved "_update_name" to HOL/Record;
2000-12-11, by wenzelm
tuned;
2000-12-11, by wenzelm
added "_update_name" and parse_translation;
2000-12-11, by wenzelm
alternative syntax for "translations": harpoons;
2000-12-11, by wenzelm
harpoons;
2000-12-11, by wenzelm
moved method lemma to BVSpec
2000-12-10, by kleing
kildall ==> wt_method for whole program
2000-12-10, by kleing
tuned;
2000-12-08, by wenzelm
unsymbolize;
2000-12-08, by wenzelm
tuned;
2000-12-07, by wenzelm
Id;
2000-12-07, by wenzelm
generate table of isabelle symbols;
2000-12-07, by wenzelm
removed Digest (temporarily, not up to date)
2000-12-07, by kleing
updated for is_class changes
2000-12-07, by kleing
removed two intermediate comments
2000-12-07, by oheimb
fixed and cleaned up wt[l]_jvm_prog proofs
2000-12-07, by kleing
tuned;
2000-12-07, by wenzelm
update for changes in Correct.thy and class/is_class defs
2000-12-07, by kleing
strengthened invariant: current class must be defined
2000-12-07, by kleing
update for changes in Step.thy
2000-12-07, by kleing
invoked class must be defined in Invoke C ...
2000-12-07, by kleing
unsymbolize;
2000-12-06, by wenzelm
left_minus axiom;
2000-12-06, by wenzelm
tuned;
2000-12-06, by wenzelm
activate Rational_Numbers;
2000-12-06, by wenzelm
deactivate Rational_Numbers (tmp!);
2000-12-06, by wenzelm
updated;
2000-12-06, by wenzelm
Rational_Numbers;
2000-12-06, by wenzelm
less rude treatment of "no_def";
2000-12-06, by wenzelm
added Library/Rational_Numbers.thy;
2000-12-06, by wenzelm
improved superclass entry for classes and definition status of is_class, class
2000-12-06, by oheimb
improved superclass entry for classes and definition status of is_class, class
2000-12-06, by oheimb
simplified interactive handling
2000-12-06, by oheimb
some derived properties;
2000-12-06, by bauerg
HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;
2000-12-06, by bauerg
*** empty log message ***
2000-12-06, by nipkow
converted rinv and hrinv to inverse;
2000-12-06, by bauerg
converted rinv to inverse;
2000-12-06, by bauerg
added \<a> ... \<z>;
2000-12-06, by wenzelm
tuned;
2000-12-06, by wenzelm
theory file for Numbers section
2000-12-06, by paulson
auto generated
2000-12-06, by paulson
auto update
2000-12-06, by paulson
deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and
2000-12-06, by paulson
miniscoping of nat_diff_split
2000-12-06, by paulson
new theory Numbers.thy
2000-12-05, by paulson
new package amsfonts
2000-12-05, by paulson
tidying
2000-12-05, by paulson
partial numerics section
2000-12-05, by paulson
nat and int sections but no real
2000-12-05, by paulson
fixed document preparation
2000-12-05, by kleing
BCV Integration
2000-12-05, by kleing
jvm_progs now also store maximum op_stack depth
2000-12-05, by kleing
*** empty log message ***
2000-12-05, by nipkow
*** empty log message ***
2000-12-04, by wenzelm
updated;
2000-12-04, by wenzelm
proper order of symbols for genarated table in system manual;
2000-12-04, by wenzelm
added \isabeginpar, \isaendpar;
2000-12-04, by wenzelm
proper order of modes;
2000-12-04, by wenzelm
diagnostic commands: comment;
2000-12-04, by wenzelm
export get_skolem;
2000-12-04, by wenzelm
fixed binding of parameters;
2000-12-04, by wenzelm
dignostic commands: comment;
2000-12-04, by wenzelm
include table of Isabelle standard symbols;
2000-12-04, by wenzelm
loads the new theory Numbers.thy
2000-12-04, by paulson
fixed formatting in section heading
2000-12-04, by paulson
auto update
2000-12-04, by paulson
tuned;
2000-12-01, by wenzelm
Now adjusted to mixed terms involving coercions.
2000-12-01, by nipkow
Linear arithmetic now copes with mixed nat/int formulae.
2000-12-01, by nipkow
append print modes;
2000-12-01, by wenzelm
no_brackets mode;
2000-12-01, by wenzelm
use_dir: modes;
2000-12-01, by wenzelm
append print_modes;
2000-12-01, by wenzelm
ignore quick_and_dirty for coind;
2000-12-01, by wenzelm
FreeUltrafilterNat ("\\<U>");
2000-12-01, by wenzelm
schematic goals;
2000-12-01, by wenzelm
removed quick_and_dirty;
2000-12-01, by wenzelm
superscripts: syntax (latex);
2000-12-01, by wenzelm
usedir: -m option;
2000-12-01, by wenzelm
added \mathcal A-Z;
2000-12-01, by wenzelm
option -m;
2000-12-01, by wenzelm
*** empty log message ***
2000-12-01, by nipkow
*** empty log message ***
2000-12-01, by nipkow
many new div and mod properties (borrowed from Integ/IntDiv)
2000-12-01, by paulson
renamed less_eq_Suc_add to less_imp_Suc_add
2000-12-01, by paulson
tuned;
2000-11-30, by wenzelm
removed "./configure";
2000-11-30, by wenzelm
/usr/bin/env bash;
2000-11-30, by wenzelm
schematic props;
2000-11-30, by wenzelm
removed get_goal;
2000-11-30, by wenzelm
added is_replaced_dummy_pattern;
2000-11-30, by wenzelm
renamed "equivalence_class" to "class";
2000-11-30, by wenzelm
schematic goals;
2000-11-30, by wenzelm
cases/induct: tuned handling of facts ('consumes');
2000-11-30, by wenzelm
'consumes' att;
2000-11-30, by wenzelm
misc;
2000-11-30, by wenzelm
replaced Eps by SOME
2000-11-30, by paulson
*** empty log message ***
2000-11-30, by nipkow
some properties;
2000-11-30, by bauerg
*** empty log message ***
2000-11-30, by nipkow
resolveq_cases_tac moved here from Pure/Isar/method.ML;
2000-11-29, by wenzelm
resolveq(_cases)_tac moved to HOL/Tools/induct_method.ML;
2000-11-29, by wenzelm
expand_split_asm -> split_split_asm
2000-11-29, by nipkow
*** empty log message ***
2000-11-29, by nipkow
*** empty log message ***
2000-11-29, by nipkow
simproc for cancelling common factors around = < <= div /
2000-11-29, by paulson
invoking CancelNumeralFactorFun
2000-11-29, by paulson
new simproc file cancel_numeral_factor.ML
2000-11-29, by paulson
added a reference to {sec:products} for ordered pair reasoning
2000-11-28, by paulson
fixed hostname;
2000-11-28, by wenzelm
detect CVSROOT;
2000-11-28, by wenzelm
tuned;
2000-11-28, by wenzelm
added consumes, consumes_default;
2000-11-28, by wenzelm
resolveq_cases_tac: insert facts;
2000-11-28, by wenzelm
added "consumes" attribute;
2000-11-28, by wenzelm
consume facts;
2000-11-28, by wenzelm
consumes0/1;
2000-11-28, by wenzelm
RuleCases.save;
2000-11-28, by wenzelm
*** empty log message ***
2000-11-27, by nipkow
deleted unused result intrel_refl
2000-11-27, by paulson
*** empty log message ***
2000-11-27, by nipkow
*** empty log message ***
2000-11-26, by nipkow
*** empty log message ***
2000-11-26, by nipkow
hide many names from Datatype_Universe.
2000-11-24, by nipkow
exception Interrupt = SML90.Interrupt;
2000-11-24, by wenzelm
added exception Interrupt for use in function Library/try
2000-11-24, by paulson
arith_tac: atomize;
2000-11-23, by wenzelm
standard: close_derivation;
2000-11-23, by wenzelm
* HOL: syntax or "abs";
2000-11-23, by wenzelm
*** empty log message ***
2000-11-23, by nipkow
tuned;
2000-11-22, by wenzelm
tuned;
2000-11-22, by wenzelm
*** empty log message ***
2000-11-22, by wenzelm
*** empty log message ***
2000-11-22, by nipkow
tag result with name reference to final binding (basically just a comment);
2000-11-21, by wenzelm
Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;
2000-11-21, by wenzelm
replace \<dots>;
2000-11-21, by wenzelm
unsymbolize;
2000-11-21, by wenzelm
quote executable;
2000-11-21, by wenzelm
tuned;
2000-11-21, by wenzelm
;
2000-11-21, by bauerg
adjusted for BV changes (Ok -> OK)
2000-11-21, by kleing
thebibliography environment: replaced the Springer version by the standard one
2000-11-21, by paulson
alternative function definition;
2000-11-21, by bauerg
*** empty log message ***
2000-11-21, by nipkow
BCV integration (type system is semilattice)
2000-11-20, by kleing
BCV integration (first step)
2000-11-20, by kleing
export freeze_thaw_type;
2000-11-18, by wenzelm
improved messages;
2000-11-18, by wenzelm
default_intro_classes_tac: Tactic.distinct_subgoals_tac;
2000-11-18, by wenzelm
axclass ordered_ring;
2000-11-18, by wenzelm
quot_cond_function: simplified, support conditional definition;
2000-11-18, by wenzelm
abs_eq_0: #0 instead of 0;
2000-11-18, by wenzelm
symbol syntax for "abs";
2000-11-18, by wenzelm
added axclass ordered_field;
2000-11-18, by wenzelm
check result: Envir.beta_norm;
2000-11-17, by wenzelm
Envir.beta_norm;
2000-11-17, by wenzelm
added beta_norm;
2000-11-17, by wenzelm
tuned;
2000-11-17, by wenzelm
removed quot_cond_function1, quot_function1;
2000-11-17, by wenzelm
UNIV_witness;
2000-11-17, by wenzelm
Ring_and_Field;
2000-11-17, by wenzelm
Library/Ring_and_Field.thy;
2000-11-17, by wenzelm
rings and fields;
2000-11-16, by bauerg
Proof.assert_forward;
2000-11-16, by wenzelm
added not_equiv_sym, not_equiv_trans1/2;
2000-11-16, by wenzelm
added abs_mult, abs_eq_0, square_nonzero;
2000-11-16, by wenzelm
ground terms section: new intro
2000-11-16, by paulson
CTT
2000-11-16, by paulson
separate rules for function/operation definitions;
2000-11-15, by wenzelm
renamed integ_le_less to int_le_less;
2000-11-15, by wenzelm
updated;
2000-11-15, by wenzelm
isabellebody: \par at begin/end;
2000-11-15, by wenzelm
auto update
2000-11-14, by paulson
first version of Advanced Inductive Defs section
2000-11-14, by paulson
x-symbol support for Pi, Sigma, -->, : (membership)
2000-11-14, by paulson
new Main.thy as in HOL, ZF
2000-11-14, by paulson
added read_terms, read_props (simulataneous type-inference);
2000-11-13, by wenzelm
tuned statement args;
2000-11-13, by wenzelm
tuned IsarThy.theorem_i;
2000-11-13, by wenzelm
added students
2000-11-13, by kleing
Removed > and >=
2000-11-13, by nipkow
Removed > and >= again.
2000-11-13, by nipkow
quot_cond_definition;
2000-11-12, by wenzelm
simplified induction;
2000-11-12, by wenzelm
updated;
2000-11-12, by wenzelm
"induct" method: handle proper rules;
2000-11-12, by wenzelm
removed warning for "stripped" option;
2000-11-12, by wenzelm
removed junk;
2000-11-12, by wenzelm
Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;
2000-11-12, by wenzelm
* added overloaded operations "inverse" and "divide" (infix "/");
2000-11-10, by wenzelm
int_distrib;
2000-11-10, by wenzelm
nat_distrib;
2000-11-10, by wenzelm
hide_space(_i): use Sign.certify_tycon, Sign.certify_tyabbr, Sign.certify_const;
2000-11-10, by wenzelm
tuned;
2000-11-10, by wenzelm
use inverse, divide from basic HOL;
2000-11-10, by wenzelm
norm_hhf_tac;
2000-11-10, by wenzelm
rewrite_goal_tac moved to tactic.ML;
2000-11-10, by wenzelm
added rewrite_goal_tac;
2000-11-10, by wenzelm
added certify_tycon, certify_tyabbr, certify_const;
2000-11-10, by wenzelm
has_meta_prems: include "==";
2000-11-10, by wenzelm
store_standard_thm "norm_hhf_eq";
2000-11-10, by wenzelm
proper theory context for mesontest2;
2000-11-10, by wenzelm
inductive_rulify2 accomodates malformed induction rules;
2000-11-10, by wenzelm
Sign.certify_tycon, Sign.certify_const;
2000-11-10, by wenzelm
improved cong_definition theorems;
2000-11-10, by wenzelm
simplified induction;
2000-11-10, by wenzelm
added axclass power (from HOL.thy);
2000-11-10, by wenzelm
simplified atomize;
2000-11-10, by wenzelm
axclass power moved to Nat.thy;
2000-11-10, by wenzelm
added axclass inverse and consts inverse, divide (infix "/");
2000-11-10, by wenzelm
FOL_basic_ss: simprocs moved to FOL_ss;
2000-11-10, by wenzelm
added atomize_eq;
2000-11-10, by wenzelm
val atomize = thms "atomize'";
2000-11-10, by wenzelm
> etc
2000-11-10, by nipkow
new: > and >=
2000-11-10, by nipkow
rule inversion
2000-11-10, by nipkow
JMB -> JMPB. Email von Johannes Pfeifroth.
2000-11-10, by nipkow
updated;
2000-11-09, by wenzelm
fixed \title: convert "_" to "-";
2000-11-09, by wenzelm
tuned isabelle environment;
2000-11-08, by wenzelm
subgoals
2000-11-08, by nipkow
*** empty log message ***
2000-11-08, by nipkow
better discussion of rule induction
2000-11-07, by paulson
Thm.dest_abs now takes an additional argument.
2000-11-07, by berghofe
Moved rewriting functions from Thm to MetaSimplifier.
2000-11-07, by berghofe
- Moved rewriting functions to meta_simplifier.ML
2000-11-07, by berghofe
moved rewriting functions from Drule to MetaSimplifier
2000-11-07, by berghofe
- new theorems imp_cong and swap_prems_eq
2000-11-07, by berghofe
Added new file meta_simplifier.ML
2000-11-07, by berghofe
Moved meta simplification stuff from Thm to MetaSimplifier.
2000-11-07, by berghofe
Added type constraint in theorem "lift".
2000-11-07, by berghofe
*** empty log message ***
2000-11-07, by nipkow
method 'induct' now handles non-atomic goals;
2000-11-06, by wenzelm
improved: 'induct' handle non-atomic goals;
2000-11-06, by wenzelm
make: open_parms argument;
2000-11-06, by wenzelm
RuleCases.make true;
2000-11-06, by wenzelm
added rewrite_goal_tac;
2000-11-06, by wenzelm
added typ_instance;
2000-11-06, by wenzelm
Sign.typ_instance;
2000-11-06, by wenzelm
inductive_atomize, inductive_rulify;
2000-11-06, by wenzelm
* Isar/HOL: method 'induct' now handles non-atomic goals; as a
2000-11-06, by wenzelm
tuned atomize_goal;
2000-11-06, by wenzelm
minor modifications for new Springer style
2000-11-06, by paulson
minor changes
2000-11-06, by paulson
auto update
2000-11-06, by paulson
*** empty log message ***
2000-11-06, by nipkow
updated;
2000-11-04, by wenzelm
tuned method "rule" and "default";
2000-11-04, by wenzelm
isamarkup: handle % in input;
2000-11-04, by wenzelm
tuned;
2000-11-04, by wenzelm
misc stuff;
2000-11-04, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-512
+512
+1000
+3000
+10000
+30000
tip