Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+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 JavaScriptenabled browsers.
register match functions from domain_constructors.ML
20100227, by huffman
move definition of match combinators to domain_constructors.ML
20100227, by huffman
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iffstyle
20100227, by huffman
move definition of discriminators to domain_constructors.ML
20100227, by huffman
move proofs of when_rews intro domain_constructors.ML
20100227, by huffman
moved proofs of dist_les and dist_eqs to domain_constructors.ML
20100227, by huffman
move proofs of casedist into domain_constructors.ML
20100227, by huffman
move proofs of injects and inverts to domain_constructors.ML
20100226, by huffman
reuse vars_of function
20100226, by huffman
remove unnecessary stuff from argument to add_constructors function
20100226, by huffman
reorder sections
20100226, by huffman
move proof of con_rews into domain_constructor.ML
20100226, by huffman
don't bother returning con_defs
20100226, by huffman
move constructorspecific stuff to a separate function
20100226, by huffman
replace prove_thm function
20100226, by huffman
move proof of compactness rules into domain_constructors.ML
20100226, by huffman
add some convenience functions
20100226, by huffman
rewrite domain package code for selector functions
20100225, by huffman
add function beta_of_def
20100224, by huffman
reorganizing domain package code (in progress)
20100224, by huffman
change domain package's treatment of variable names in theorems to be like datatype package
20100224, by huffman
remove redundant lemma real_minus_half_eq
20100224, by huffman
polished and converted some proofs to Isar style
20100224, by huffman
killed more recdefs
20100302, by krauss
tuned comment
20100301, by krauss
repaired subscripts broken in d8d7d1b785af
20100302, by haftmann
repaired definition (cf. d8d7d1b785af)
20100302, by haftmann
authentic syntax for *all* logical entities;
20100303, by wenzelm
mark_atoms: more precise treatment of SynExt.standard_token_markers vs. syntax consts;
20100303, by wenzelm
notation for xsymbols (cf. ad039d29e01c);
20100303, by wenzelm
"_type_prop" is syntax const  recovered printing of OFCLASS;
20100303, by wenzelm
removed unused external_names;
20100303, by wenzelm
cleanup type translations;
20100303, by wenzelm
adapted to authentic syntax  actual types are verbatim;
20100303, by wenzelm
authentic syntax for classes and type constructors;
20100303, by wenzelm
more systematic mark/unmark operations;
20100303, by wenzelm
proper (type_)notation;
20100302, by wenzelm
proper antiquotations;
20100302, by wenzelm
standard convention for syntax consts;
20100302, by wenzelm
more precise scope of exception handler;
20100302, by wenzelm
eliminated hard tabs;
20100301, by wenzelm
tuned final whitespace;
20100301, by wenzelm
repaired 'definition' (cf. d8d7d1b785af);
20100301, by wenzelm
merged
20100301, by wenzelm
more recdef (and old primrec) hunting
20100301, by krauss
killed recdefs in HOLAuth
20100301, by krauss
merged
20100301, by haftmann
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
20100301, by haftmann
export add_quotient_type.
20100301, by Cezary Kaliszyk
updated generated files;
20100301, by wenzelm
added type_notation command;
20100301, by wenzelm
more uniform treatment of syntax for types vs. consts;
20100301, by wenzelm
made smlnj happy
20100301, by bulwahn
more antiquotations;
20100228, by wenzelm
more antiquotations;
20100228, by wenzelm
modernized structure Term_Ord;
20100227, by wenzelm
use existing Typ_Graph;
20100227, by wenzelm
further standard instances of functor Graph;
20100227, by wenzelm
code simplification by inlining;
20100227, by wenzelm
just one copy of structure Term_Graph (in Pure);
20100227, by wenzelm
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip