isabelle: Graph

merged
2010-03-03, by bulwahn
made smlnj happy
2010-03-02, by bulwahn
adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
2010-03-02, by bulwahn
adding HOL-Mutabelle to tests
2010-03-02, by bulwahn
merged
2010-03-03, by haftmann
more explicit naming scheme
2010-03-03, by haftmann
merged
2010-03-02, by huffman
adapt to changed variable name in casedist theorem
2010-03-02, by huffman
remove dependency on domain_syntax.ML
2010-03-02, by huffman
update HOLCF makefile
2010-03-02, by huffman
simplify add_axioms function; remove obsolete domain_syntax.ML
2010-03-02, by huffman
proof scripts use variable name y for casedist
2010-03-02, by huffman
fixrec and repdef modules import holcf_library
2010-03-02, by huffman
use y as variable name in casedist, like datatype package
2010-03-02, by huffman
proper names for types cfun, sprod, ssum
2010-03-02, by huffman
variable name changed
2010-03-02, by huffman
fix proof script for take_apps so it works with indirect recursion
2010-03-02, by huffman
remove dead code
2010-03-02, by huffman
remove unused mixfix component from type cons
2010-03-02, by huffman
cleaned up, added type annotations
2010-03-02, by huffman
remove unused selector field from type arg
2010-03-02, by huffman
add_syntax no longer needs a definitional mode
2010-03-02, by huffman
add_axioms no longer needs a definitional mode
2010-03-02, by huffman
get rid of primes on thy variables
2010-03-02, by huffman
move definition of finiteness predicate into domain_take_proofs.ML
2010-03-02, by huffman
move take-related definitions and proofs to new module; simplify map_of_typ functions
2010-03-02, by huffman
remove map_tab argument to calc_axioms
2010-03-02, by huffman
remove dead code
2010-03-02, by huffman
merged
2010-03-02, by paulson
Slightly generalised a theorem
2010-03-02, by paulson
merged
2010-03-02, by paulson
merged
2010-02-19, by paulson
merged
2010-02-19, by paulson
merged
2010-02-05, by paulson
merged
2010-02-04, by paulson
merged
2010-02-02, by paulson
Correction of a tiny error
2010-02-02, by paulson
removed obsolete helper theory
2010-03-02, by krauss
merged
2010-03-02, by haftmann
dropped superfluous naming
2010-03-02, by haftmann
UNIV is not a logical constant
2010-03-02, by huffman
merged
2010-03-02, by huffman
re-enable bisim code, now in domain_theorems.ML
2010-03-02, by huffman
add missing rule to case_strict proof script
2010-03-02, by huffman
remove dead code
2010-03-02, by huffman
domain package no longer generates copy functions; all proofs use take functions instead
2010-03-02, by huffman
need to explicitly include REP_convex
2010-03-01, by huffman
add lemma lub_eq
2010-03-01, by huffman
add lemmas about ssum_map and sprod_map
2010-03-01, by huffman
generate take_take rules
2010-03-01, by huffman
add function define_take_functions
2010-03-01, by huffman
add missing strictify rule to proof script
2010-03-01, by huffman
qualify constructor names with type name
2010-03-01, by huffman
move definition of case combinator to domain_constructors.ML
2010-03-01, by huffman
remove dependence on Domain_Library
2010-03-01, by huffman
more uses of function get_vars
2010-03-01, by huffman
add functions get_vars, get_vars_avoiding
2010-03-01, by huffman
move proofs of pat_rews to domain_constructors.ML
2010-03-01, by huffman
add_domain_constructors takes iso_info record as argument
2010-02-28, by huffman
domain_isomorphism package proves deflation rules for map functions
2010-02-28, by huffman
store deflation thms for map functions in theory data
2010-02-28, by huffman
use function list_ccomb
2010-02-28, by huffman
add function define_const
2010-02-28, by huffman
fix infix declarations
2010-02-28, by huffman
move common functions into new file holcf_library.ML
2010-02-28, by huffman
get rid of incomplete pattern match warnings
2010-02-28, by huffman
move some powerdomain stuff into a new file
2010-02-28, by huffman
move case combinator syntax to domain_constructors.ML
2010-02-28, by huffman
remove redundant code
2010-02-28, by huffman
use correct syntax name for pattern combinator
2010-02-28, by huffman
fix output translation for Case syntax
2010-02-28, by huffman
move definition and syntax of pattern combinators into domain_constructors.ML
2010-02-28, by huffman
domain_isomorphism function returns iso_info record
2010-02-27, by huffman
move proofs of match_rews to domain_constructors.ML
2010-02-27, by huffman
remove dead code
2010-02-27, by huffman
removed dead code
2010-02-27, by huffman
register match functions from domain_constructors.ML
2010-02-27, by huffman
move definition of match combinators to domain_constructors.ML
2010-02-27, by huffman
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iff-style
2010-02-27, by huffman
move definition of discriminators to domain_constructors.ML
2010-02-27, by huffman
move proofs of when_rews intro domain_constructors.ML
2010-02-27, by huffman
moved proofs of dist_les and dist_eqs to domain_constructors.ML
2010-02-27, by huffman
move proofs of casedist into domain_constructors.ML
2010-02-27, by huffman
move proofs of injects and inverts to domain_constructors.ML
2010-02-26, by huffman
reuse vars_of function
2010-02-26, by huffman
remove unnecessary stuff from argument to add_constructors function
2010-02-26, by huffman
reorder sections
2010-02-26, by huffman
move proof of con_rews into domain_constructor.ML
2010-02-26, by huffman
don't bother returning con_defs
2010-02-26, by huffman
move constructor-specific stuff to a separate function
2010-02-26, by huffman
replace prove_thm function
2010-02-26, by huffman
move proof of compactness rules into domain_constructors.ML
2010-02-26, by huffman
add some convenience functions
2010-02-26, by huffman
rewrite domain package code for selector functions
2010-02-25, by huffman
add function beta_of_def
2010-02-24, by huffman
reorganizing domain package code (in progress)
2010-02-24, by huffman
change domain package's treatment of variable names in theorems to be like datatype package
2010-02-24, by huffman
remove redundant lemma real_minus_half_eq
2010-02-24, by huffman
polished and converted some proofs to Isar style
2010-02-24, by huffman
killed more recdefs
2010-03-02, by krauss
tuned comment
2010-03-01, by krauss
repaired subscripts broken in d8d7d1b785af
2010-03-02, by haftmann
repaired definition (cf. d8d7d1b785af)
2010-03-02, by haftmann
authentic syntax for *all* logical entities;
2010-03-03, by wenzelm
mark_atoms: more precise treatment of SynExt.standard_token_markers vs. syntax consts;
2010-03-03, by wenzelm
notation for xsymbols (cf. ad039d29e01c);
2010-03-03, by wenzelm
"_type_prop" is syntax const -- recovered printing of OFCLASS;
2010-03-03, by wenzelm
removed unused external_names;
2010-03-03, by wenzelm
cleanup type translations;
2010-03-03, by wenzelm
adapted to authentic syntax -- actual types are verbatim;
2010-03-03, by wenzelm
authentic syntax for classes and type constructors;
2010-03-03, by wenzelm
more systematic mark/unmark operations;
2010-03-03, by wenzelm
proper (type_)notation;
2010-03-02, by wenzelm
proper antiquotations;
2010-03-02, by wenzelm
standard convention for syntax consts;
2010-03-02, by wenzelm
more precise scope of exception handler;
2010-03-02, by wenzelm
eliminated hard tabs;
2010-03-01, by wenzelm
tuned final whitespace;
2010-03-01, by wenzelm
repaired 'definition' (cf. d8d7d1b785af);
2010-03-01, by wenzelm
merged
2010-03-01, by wenzelm
more recdef (and old primrec) hunting
2010-03-01, by krauss
killed recdefs in HOL-Auth
2010-03-01, by krauss
merged
2010-03-01, by haftmann
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-03-01, by haftmann
export add_quotient_type.
2010-03-01, by Cezary Kaliszyk
updated generated files;
2010-03-01, by wenzelm
added type_notation command;
2010-03-01, by wenzelm
more uniform treatment of syntax for types vs. consts;
2010-03-01, by wenzelm
made smlnj happy
2010-03-01, by bulwahn
more antiquotations;
2010-02-28, by wenzelm
more antiquotations;
2010-02-28, by wenzelm
modernized structure Term_Ord;
2010-02-27, by wenzelm
use existing Typ_Graph;
2010-02-27, by wenzelm
further standard instances of functor Graph;
2010-02-27, by wenzelm
code simplification by inlining;
2010-02-27, by wenzelm
just one copy of structure Term_Graph (in Pure);
2010-02-27, by wenzelm
modernized structure Int_Graph;
2010-02-27, by wenzelm
clarified @{const_name} vs. @{const_abbrev};
2010-02-27, by wenzelm
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
2010-02-27, by wenzelm
type/const name: explicitly allow abbreviations as well;
2010-02-27, by wenzelm
clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
2010-02-27, by wenzelm
added at-poly-test, which is intended for performance tests of Poly/ML itself;
2010-02-27, by wenzelm
more precise syntax antiquotations;
2010-02-27, by wenzelm
ML antiquotations for type classes;
2010-02-27, by wenzelm
read_class: perform actual read, with source position;
2010-02-27, by wenzelm
parallel brute-force disambiguation;
2010-02-27, by wenzelm
degrade gracefully in CRITICAL section;
2010-02-27, by wenzelm
gen_dest_case: recovered @{const_name} from c8a6fae0ad0c, because of separate Syntax.mark_const in case_tr' -- avoid extra syntax markers in output;
2010-02-26, by wenzelm
tuned;
2010-02-26, by wenzelm
use simplified Syntax.escape;
2010-02-26, by wenzelm
tuned hyp_subst_tac';
2010-02-26, by wenzelm
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
2010-02-26, by blanchet
merged
2010-02-26, by blanchet
more work on the new monotonicity stuff in Nitpick
2010-02-26, by blanchet
improved precision of infinite "shallow" datatypes in Nitpick;
2010-02-25, by blanchet
cosmetics
2010-02-25, by blanchet
merged
2010-02-26, by bulwahn
merged
2010-02-26, by bulwahn
adding no_topmost_reordering as new option to the code_pred command
2010-02-25, by bulwahn
adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
2010-02-25, by bulwahn
added quiet option to quickcheck command
2010-02-25, by bulwahn
added basic reporting of test cases to quickcheck
2010-02-25, by bulwahn
merged
2010-02-26, by haftmann
use abstract code cerficates for bare code theorems
2010-02-26, by haftmann
implement quotient_of for odl SML code generator
2010-02-26, by haftmann
adjusted to cs. e4a7947e02b8
2010-02-26, by haftmann
bound argument for abstype proposition
2010-02-24, by haftmann
renamed theory Rational to Rat
2010-02-24, by haftmann
tuned whitespace
2010-02-24, by haftmann
more precise exception handler
2010-02-24, by haftmann
more general case and induct rules; normalize and quotient_of; abstract code generation
2010-02-24, by haftmann
crossproduct coprimality lemmas
2010-02-24, by haftmann
lemma div_mult_swap, dvd_div_eq_mult, dvd_div_div_eq_mult
2010-02-24, by haftmann
evaluation for abstypes
2010-02-24, by haftmann
modernized structure Split_Rule;
2010-02-25, by wenzelm
more antiquotations;
2010-02-25, by wenzelm
explicit @{type_syntax} markup;
2010-02-25, by wenzelm
explicit @{type_syntax} markup;
2010-02-25, by wenzelm
more orthogonal antiquotations for type constructors;
2010-02-25, by wenzelm
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
2010-02-25, by wenzelm
provide direct access to the different kinds of type declarations;
2010-02-25, by wenzelm
use mixfix syntax for Boogie types
2010-02-25, by boehmes
merged
2010-02-24, by wenzelm
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
2010-02-24, by boehmes
modernized syntax declarations, and make them actually work with authentic syntax;
2010-02-24, by wenzelm
observe standard convention for syntax consts;
2010-02-24, by wenzelm
proper type syntax (cf. 7425aece4ee3);
2010-02-24, by wenzelm
observe standard convention for syntax consts;
2010-02-24, by wenzelm
allow general mixfix syntax for type constructors;
2010-02-24, by wenzelm
merged
2010-02-24, by huffman
merged
2010-02-23, by huffman
remove redundant lemma realpow_increasing
2010-02-23, by huffman
remove redundant simp rules from RealPow.thy
2010-02-23, by huffman
adapt to new realpow rules
2010-02-23, by huffman
adapt to changes in simpset
2010-02-23, by huffman
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
2010-02-23, by huffman
move float syntax from RealPow to Rational
2010-02-23, by huffman
compile
2010-02-24, by blanchet
merged
2010-02-24, by blanchet
compile
2010-02-24, by blanchet
make example compile
2010-02-24, by blanchet
got rid of "axclass", apparently
2010-02-24, by blanchet
merged
2010-02-24, by blanchet
cosmetics
2010-02-24, by blanchet
support local definitions in Nitpick
2010-02-23, by blanchet
show Kodkod warning message even in non-verbose mode
2010-02-23, by blanchet
distinguish between Kodkodi warnings and errors in Nitpick;
2010-02-23, by blanchet
optimized multisets in Nitpick by fishing "finite"
2010-02-23, by blanchet
document Quickcheck's "no_assms" option
2010-02-23, by blanchet
tuned comment
2010-02-24, by haftmann
merged
2010-02-23, by hoelzl
Moved old Integration to examples.
2010-02-23, by hoelzl
merged
2010-02-23, by bulwahn
merged
2010-02-23, by bulwahn
adding ROOT.ML to HOL-Mutabelle session; uncommenting HOL.induct constants in Mutabelle session
2010-02-23, by bulwahn
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
2010-02-23, by bulwahn
separated narrowing timeouts for intermediate and final steps
2010-02-23, by boehmes
merged
2010-02-23, by haftmann
merged
2010-02-23, by haftmann
dropped axclass; dropped Id; session theory Hoare.thy
2010-02-23, by haftmann
dropped session W0; c.f. MiniML in AFP
2010-02-23, by haftmann
dropped axclass, going back to purely syntactic type classes
2010-02-23, by haftmann
dropped axclass; dropped Id
2010-02-23, by haftmann
dropped axclass; dropped Id; session theory Hoare.thy
2010-02-23, by haftmann
dropped axclass
2010-02-23, by haftmann
export prs_rules and rsp_rules attributes
2010-02-23, by Cezary Kaliszyk
merge
2010-02-23, by blanchet
improved precision of small sets in Nitpick
2010-02-23, by blanchet
improved Nitpick's support for quotient types
2010-02-23, by blanchet
Forgot to check NSA in changeset e4a431b6d9b7 ; Removed import of Integration
2010-02-23, by hoelzl
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
2010-02-23, by blanchet
mind the "s"
2010-02-23, by haftmann
merged
2010-02-23, by haftmann
NEWS
2010-02-22, by haftmann
added missing separator
2010-02-22, by haftmann
more accurate when registering new types
2010-02-22, by haftmann
added Dlist
2010-02-22, by haftmann
tuned text
2010-02-22, by haftmann
distributed theory Algebras to theories Groups and Lattices
2010-02-22, by haftmann
merged
2010-02-22, by haftmann