Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+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.
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
tuned;
2000-11-03, by wenzelm
proper setup of "parallel";
2000-11-03, by wenzelm
tuned notation;
2000-11-03, by wenzelm
adapted "obtain" proofs;
2000-11-03, by wenzelm
provide case names for rev_induct, rev_cases;
2000-11-03, by wenzelm
rev_exhaust: rulify;
2000-11-03, by wenzelm
removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);
2000-11-03, by wenzelm
"atomize" for classical tactics;
2000-11-03, by wenzelm
atomize: all automated tactics that "solve" goals;
2000-11-03, by wenzelm
fixed two obscurities of "fix": predeclare_terms;
2000-11-03, by wenzelm
tuned names;
2000-11-03, by wenzelm
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
removed Acc and Multiset (see HOL/Library);
2000-10-18, by wenzelm
moved to HOL/Library;
2000-10-18, by wenzelm
MultisetOrder mmoved to HOL/Library;
2000-10-18, by wenzelm
moved to HOL/LIbrary;
2000-10-18, by wenzelm
added HOL/Library, rearranged several files;
2000-10-18, by wenzelm
moved to HOL/Library;
2000-10-18, by wenzelm
"The Supplemental Isabelle/HOL Library";
2000-10-18, by wenzelm
added path_add;
2000-10-18, by wenzelm
A general ``while'' combinator (from main HOL);
2000-10-18, by wenzelm
Quotient types;
2000-10-18, by wenzelm
Multisets (from HOL/Induct/Multiset and friends);
2000-10-18, by wenzelm
The accessible part of a relation (from HOL/Induct/Acc);
2000-10-18, by wenzelm
\isabellecontext: output_syms;
2000-10-18, by wenzelm
restart: do not reset theory loader path;
2000-10-18, by wenzelm
* HOL/Library: a collection of generic theories to be used together
2000-10-18, by wenzelm
*** empty log message ***
2000-10-18, by nipkow
*** empty log message ***
2000-10-18, by nipkow
*** empty log message ***
2000-10-18, by nipkow
wellfounded -> well-founded
2000-10-18, by paulson
tuned;
2000-10-17, by wenzelm
"Deriving rules";
2000-10-17, by wenzelm
improved;
2000-10-17, by wenzelm
*** empty log message ***
2000-10-17, by nipkow
*** empty log message ***
2000-10-17, by nipkow
renaming of contrapos rules
2000-10-17, by paulson
tidied some awkward proofs
2000-10-17, by paulson
tidying; removed unused rev_contra_subsetD
2000-10-17, by paulson
restoration of "equalityI"; renaming of contrapos rules
2000-10-17, by paulson
renaming of contrapos rules
2000-10-17, by paulson
tidying and renaming of contrapos rules
2000-10-17, by paulson
cosmetics
2000-10-17, by oheimb
added intermediate value thms
2000-10-17, by nipkow
<= -> \<le>
2000-10-17, by nipkow
updated;
2000-10-16, by wenzelm
*** empty log message ***
2000-10-16, by nipkow
*** empty log message ***
2000-10-16, by nipkow
tuned;
2000-10-15, by wenzelm
fixed \isasyminv;
2000-10-15, by wenzelm
more elements;
2000-10-15, by wenzelm
proper symbol markup with \isamath, \isatext;
2000-10-15, by wenzelm
*** empty log message ***
2000-10-13, by nipkow
*** empty log message ***
2000-10-13, by nipkow
*** empty log message ***
2000-10-13, by nipkow
renamed fp_Tarski to fp_unfold
2000-10-13, by paulson
*** empty log message ***
2000-10-13, by nipkow
*** empty log message ***
2000-10-13, by nipkow
*** empty log message ***
2000-10-12, by nipkow
*** empty log message ***
2000-10-12, by nipkow
updated;
2000-10-12, by wenzelm
induct -> lfp_induct;
2000-10-12, by wenzelm
install default_handler for SIGINT initially as well;
2000-10-12, by wenzelm
tuned syms;
2000-10-12, by wenzelm
updated;
2000-10-12, by wenzelm
accomodate Poly/ML 4.0;
2000-10-12, by wenzelm
even smarter setup for several installations of Poly/ML 3.x and 4.0;
2000-10-12, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip