Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-120
+120
+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.
improved handling of "that": insert into goal, only declare as Pure "intro";
2000-11-03, by wenzelm
assumption / finish: handle non-atomic assumptions from context as well;
2000-11-03, by wenzelm
added atomic_judgment;
2000-11-03, by wenzelm
structure Obtain = Obtain;
2000-11-03, by wenzelm
new lemma card_Diff2_less for mulilated chess board
2000-11-03, by paulson
*** empty log message ***
2000-11-03, by nipkow
*** empty log message ***
2000-11-03, by nipkow
*** empty log message ***
2000-11-03, by nipkow
the section command will belong to the new file
2000-11-03, by paulson
advanced induction examples
2000-11-03, by paulson
auto update?
2000-11-03, by paulson
replaced Acc.thy by Advanced.thy
2000-11-03, by paulson
no longer needed: too complicated an example
2000-11-02, by paulson
*** empty log message ***
2000-11-02, by nipkow
auto generated
2000-11-02, by paulson
tuned goal output;
2000-10-31, by wenzelm
*** empty log message ***
2000-10-31, by nipkow
*** empty log message ***
2000-10-31, by nipkow
updated;
2000-10-30, by wenzelm
tuned goals output;
2000-10-30, by wenzelm
improved statement bindings for props;
2000-10-30, by wenzelm
converse: syntax \<inverse>;
2000-10-30, by wenzelm
tuned;
2000-10-30, by wenzelm
added ex/PER.thy;
2000-10-30, by wenzelm
improved doc of "subgoals" antiquotation;
2000-10-30, by wenzelm
replaced \isasymmacron by \isasyminverse;
2000-10-30, by wenzelm
tuned tex template;
2000-10-30, by wenzelm
Partial equivalence relations (leftover from HOL/Quot);
2000-10-30, by wenzelm
added antiq. subgoals
2000-10-30, by nipkow
Added antiquotation "subgoals".
2000-10-30, by nipkow
Mod because of additional parameters to pretty_goals.
2000-10-30, by nipkow
back to 1.167, due to Emacs/CVS casualty!!;
2000-10-27, by wenzelm
added instantiate_tac
2000-10-27, by oheimb
*** empty log message ***
2000-10-27, by wenzelm
removed isabelle resources: are available from main pages
2000-10-27, by kleing
cleanup, looks ok now with konqueror, too
2000-10-27, by kleing
*** empty log message ***
2000-10-26, by nipkow
*** empty log message ***
2000-10-26, by nipkow
added the $Id:$ line
2000-10-26, by paulson
*** empty log message ***
2000-10-26, by nipkow
*** empty log message ***
2000-10-26, by nipkow
use Library/List_Prefix;
2000-10-25, by wenzelm
added HOL/Library/List_Prefix;
2000-10-25, by wenzelm
improved antiquotations;
2000-10-25, by wenzelm
added \isarantiq;
2000-10-25, by wenzelm
add \<le> to list of "good" symbols;
2000-10-25, by wenzelm
tuned names;
2000-10-25, by wenzelm
added List_Prefix;
2000-10-25, by wenzelm
more "xsymbols" syntax;
2000-10-25, by wenzelm
"List prefixes" library theory (replaces old Lex/Prefix);
2000-10-25, by wenzelm
*** empty log message ***
2000-10-25, by nipkow
*** empty log message ***
2000-10-25, by nipkow
inputs Even.tex
2000-10-25, by paulson
minor tinkering
2000-10-25, by paulson
Even numbers section of Inductive chapter
2000-10-25, by paulson
tuned msg;
2000-10-25, by wenzelm
antiquotation "goals": error message;
2000-10-25, by wenzelm
* support sub/super scripts (for single symbols only), input syntax is
2000-10-24, by wenzelm
let commands access Toplevel.state;
2000-10-24, by wenzelm
added pretty_goals;
2000-10-24, by wenzelm
added antiquotation "goals" and option "goals_limit";
2000-10-24, by wenzelm
tuned;
2000-10-24, by wenzelm
added clasimpset: unit -> clasimpset;
2000-10-24, by wenzelm
tuned;
2000-10-24, by wenzelm
Acc example
2000-10-24, by paulson
even numbers example
2000-10-24, by paulson
intro_classes by default;
2000-10-23, by wenzelm
declare trancl rules;
2000-10-23, by wenzelm
tuned;
2000-10-23, by wenzelm
updated;
2000-10-23, by wenzelm
intro_classes by default;
2000-10-23, by wenzelm
make sure default document works;
2000-10-23, by wenzelm
comment out Pure-copied target;
2000-10-23, by wenzelm
* HOL: default proof step now includes 'intro_classes';
2000-10-23, by wenzelm
*** empty log message ***
2000-10-23, by nipkow
part of set-up
2000-10-23, by paulson
sets chapter
2000-10-23, by paulson
fixed crossref
2000-10-23, by paulson
tidied
2000-10-23, by paulson
X-symbol
2000-10-23, by paulson
auto gen
2000-10-23, by paulson
addition of Rules, Sets and some macros of lcp
2000-10-23, by paulson
goodbye to this dummy file
2000-10-23, by paulson
now includes Rules, Sets (?)
2000-10-23, by paulson
the Rules chapter and theories
2000-10-23, by paulson
the Sets chapter and theories
2000-10-23, by paulson
quantifiers now allowed in inductive defs
2000-10-23, by paulson
tidied
2000-10-23, by paulson
isatool unsymbolize;
2000-10-23, by wenzelm
added type_definitionI;
2000-10-23, by wenzelm
tuned deps;
2000-10-23, by wenzelm
contrapos
2000-10-23, by paulson
two spelling fixes
2000-10-23, by paulson
tuned;
2000-10-22, by wenzelm
simplified quotients (only plain total equivs);
2000-10-22, by wenzelm
tuned;
2000-10-20, by wenzelm
*** empty log message ***
2000-10-20, by nipkow
tuned;
2000-10-20, by wenzelm
*** empty log message ***
2000-10-20, by nipkow
provide more theorems (see subset.thy);
2000-10-19, by wenzelm
InductAttrib;
2000-10-19, by wenzelm
improved typedef;
2000-10-19, by wenzelm
improved typedef;
2000-10-19, by wenzelm
added theory for HOL type definitions;
2000-10-19, by wenzelm
tuned;
2000-10-19, by wenzelm
added Tools/induct_attrib.ML;
2000-10-19, by wenzelm
declare sym [elim?] in HOL.ML instead of Calculation.thy;
2000-10-19, by wenzelm
tuned \isasymuniqex;
2000-10-19, by wenzelm
split over two files: induct_attrib.ML, induct_method.ML;
2000-10-19, by wenzelm
tuned;
2000-10-19, by wenzelm
use RecdefPackage.tcs_of;
2000-10-19, by wenzelm
added tcs_of;
2000-10-19, by wenzelm
updated;
2000-10-18, by wenzelm
removed Library/Accessible_Part.ML;
2000-10-18, by wenzelm
use Multiset from HOL/Library;
2000-10-18, by wenzelm
use Accessible_Part from HOL/Library;
2000-10-18, by wenzelm
path_add "~~/src/HOL/Library";
2000-10-18, by wenzelm
tuned;
2000-10-18, by wenzelm
tuned declarations;
2000-10-18, by wenzelm
avoid "_" and "^" (more robust);
2000-10-18, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-120
+120
+1000
+3000
+10000
+30000
tip