| 2001-01-12 |
wenzelm |
added Sigma_Algebra;
|
changeset |
files
|
| 2001-01-12 |
wenzelm |
added Induct/Sigma_Algebra.thy;
|
changeset |
files
|
| 2001-01-12 |
wenzelm |
tuned;
|
changeset |
files
|
| 2001-01-11 |
wenzelm |
do not hilite "xnum";
|
changeset |
files
|
| 2001-01-11 |
wenzelm |
make_raw: do not AutoBind.drop_judgment;
|
changeset |
files
|
| 2001-01-11 |
wenzelm |
induct cases: RuleCases.make_raw;
|
changeset |
files
|
| 2001-01-11 |
wenzelm |
added strict_prefixI', strict_prefixE';
|
changeset |
files
|
| 2001-01-11 |
wenzelm |
subst syntax;
|
changeset |
files
|
| 2001-01-11 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2001-01-11 |
paulson |
lcp's suggestions for CTL
|
changeset |
files
|
| 2001-01-11 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2001-01-11 |
paulson |
a new label
|
changeset |
files
|
| 2001-01-11 |
paulson |
revisions corresponding to the new version of sets.tex
|
changeset |
files
|
| 2001-01-10 |
nipkow |
Added <cdot> syntax for continuous application $.
|
changeset |
files
|
| 2001-01-10 |
wenzelm |
isatool unsymbolize;
|
changeset |
files
|
| 2001-01-10 |
wenzelm |
updated;
|
changeset |
files
|
| 2001-01-10 |
wenzelm |
tuned \DOT, \DDOT;
|
changeset |
files
|
| 2001-01-10 |
wenzelm |
added \<wrong> symbol;
|
changeset |
files
|
| 2001-01-10 |
wenzelm |
tuned;
|
changeset |
files
|
| 2001-01-10 |
paulson |
revisions e.g. images, transitive closure...
|
changeset |
files
|
| 2001-01-10 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2001-01-10 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2001-01-10 |
paulson |
case_tac on bools
|
changeset |
files
|
| 2001-01-10 |
paulson |
case_tac subgoals
|
changeset |
files
|
| 2001-01-10 |
paulson |
deleted the obsolete nat_neqE (and reformatting)
|
changeset |
files
|
| 2001-01-10 |
paulson |
deleted the obsolete nat_neqE
|
changeset |
files
|
| 2001-01-10 |
paulson |
generalizing the LEAST theorems from "nat" to linear
|
changeset |
files
|
| 2001-01-10 |
paulson |
now using "by" for one-line proofs
|
changeset |
files
|
| 2001-01-10 |
paulson |
various changes including the SOME examples, rule_format and "by"
|
changeset |
files
|
| 2001-01-10 |
paulson |
loads the new theory
|
changeset |
files
|
| 2001-01-10 |
paulson |
reformatting, and splitting the end of "Primes" to create "Forward"
|
changeset |
files
|
| 2001-01-10 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2001-01-10 |
paulson |
now using "by" for one-line proofs
|
changeset |
files
|
| 2001-01-10 |
paulson |
introduction of "by" and a few examples of SOME
|
changeset |
files
|
| 2001-01-10 |
paulson |
auto update
|
changeset |
files
|
| 2001-01-10 |
paulson |
new wfrec example
|
changeset |
files
|
| 2001-01-10 |
paulson |
fixed the treatment of Rules and Sets
|
changeset |
files
|
| 2001-01-10 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2001-01-09 |
wenzelm |
use \<acute>;
|
changeset |
files
|
| 2001-01-09 |
wenzelm |
added \<dieresis>, \<acute>, \<cedilla>, \<emptyset>;
|
changeset |
files
|
| 2001-01-09 |
wenzelm |
added acute, cedilla, dieresis, hungarumlaut;
|
changeset |
files
|
| 2001-01-09 |
nipkow |
` -> $
|
changeset |
files
|
| 2001-01-09 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2001-01-09 |
nipkow |
`` -> ` and ``` -> ``
|
changeset |
files
|
| 2001-01-09 |
nipkow |
`` -> and ``` -> ``
|
changeset |
files
|
| 2001-01-09 |
wenzelm |
replaced \<macron> by \<inverse>;
|
changeset |
files
|
| 2001-01-09 |
wenzelm |
avoid renaming of params in cases;
|
changeset |
files
|
| 2001-01-09 |
wenzelm |
split_all operation;
|
changeset |
files
|
| 2001-01-09 |
oheimb |
improved evaluation judgment syntax; modified Loop rule
|
changeset |
files
|
| 2001-01-09 |
wenzelm |
syntax (xsymbols);
|
changeset |
files
|
| 2001-01-08 |
nipkow |
Removed Applyall
|
changeset |
files
|
| 2001-01-08 |
paulson |
additional pattern allows reduction of fractions to lowest terms
|
changeset |
files
|
| 2001-01-08 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 2001-01-07 |
wenzelm |
updated;
|
changeset |
files
|
| 2001-01-07 |
wenzelm |
removed ID (avoid CVS conflicts with generated versions);
|
changeset |
files
|
| 2001-01-07 |
wenzelm |
CHANGED_PROP;
|
changeset |
files
|
| 2001-01-07 |
wenzelm |
removed MicroJava/BV/Convert.thy;
|
changeset |
files
|
| 2001-01-07 |
wenzelm |
do not AutoBind.drop_judgment;
|
changeset |
files
|
| 2001-01-07 |
wenzelm |
tuned output;
|
changeset |
files
|
| 2001-01-07 |
wenzelm |
tuned norm_hhf(_tac);
|
changeset |
files
|