2009-09-21 haftmann 2009-09-21 merged
2009-09-21 haftmann 2009-09-21 tuned proof; tuned headers
2009-09-21 haftmann 2009-09-21 merged
2009-09-21 haftmann 2009-09-21 tuned proofs; be more cautios wrt. default simp rules
2009-09-21 haftmann 2009-09-21 merged
2009-09-21 haftmann 2009-09-21 tuned proofs
2009-09-19 haftmann 2009-09-19 merged
2009-09-19 haftmann 2009-09-19 inter and union are mere abbreviations for inf and sup
2009-09-24 haftmann 2009-09-24 merged
2009-09-24 haftmann 2009-09-24 lemma relating fold1 and foldl; code_unfold rules for Inf_fin, Sup_fin, Min, Max, Inf, Sup
2009-09-24 haftmann 2009-09-24 subsumed by more general setup in List.thy
2009-09-24 haftmann 2009-09-24 idempotency case for fold1
2009-09-24 haftmann 2009-09-24 added dual for complete lattice
2009-09-24 nipkow 2009-09-24 merged
2009-09-24 nipkow 2009-09-24 record how many "proof"s are solved by s/h
2009-09-24 boehmes 2009-09-24 added quotes for filenames; truncated remaining time (no floats supported by ulimit)
2009-09-24 bulwahn 2009-09-24 merged; adopted to changes from Code_Evaluation in the predicate compiler
2009-09-23 bulwahn 2009-09-23 replaced sorry by oops; removed old debug functions in predicate compiler
2009-09-23 bulwahn 2009-09-23 added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
2009-09-23 bulwahn 2009-09-23 adapted configuration for DatatypeCase.make_case
2009-09-23 bulwahn 2009-09-23 added a new example for the predicate compiler
2009-09-23 bulwahn 2009-09-23 added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
2009-09-23 bulwahn 2009-09-23 added first prototype of the extended predicate compiler
2009-09-23 bulwahn 2009-09-23 moved predicate compiler to Tools
2009-09-23 bulwahn 2009-09-23 removed generation of strange tuple modes in predicate compiler
2009-09-23 bulwahn 2009-09-23 extending predicate compiler and proof procedure to support tuples; testing predicate wirh HOL-MicroJava semantics
2009-09-23 bulwahn 2009-09-23 modified predicate compiler further to support tuples
2009-09-23 bulwahn 2009-09-23 changed preprocessing due to problems with LightweightJava; added transfer of thereoms; changed the type of mode to support tuples in the predicate compiler
2009-09-23 bulwahn 2009-09-23 handling of definitions
2009-09-23 bulwahn 2009-09-23 experimenting to add some useful interface for definitions
2009-09-23 bulwahn 2009-09-23 added predicate compile preprocessing structure for definitional thms -- probably is replaced by hooking the theorem command differently
2009-09-23 bulwahn 2009-09-23 modified handling of side conditions in proof procedure of predicate compiler
2009-09-23 haftmann 2009-09-23 merged
2009-09-23 haftmann 2009-09-23 Code_Eval(uation)
2009-09-23 blanchet 2009-09-23 merged
2009-09-23 blanchet 2009-09-23 Added "nitpick_const_simp" tags to lazy list theories. (Will be useful once Nitpick is integrated in Isabelle.)
2009-09-23 krauss 2009-09-23 atbroy101 is long dead, use atbroy99; comment out broken SML test invocation
2009-09-23 haftmann 2009-09-23 merged
2009-09-23 haftmann 2009-09-23 stripped legacy ML bindings
2009-09-23 hoelzl 2009-09-23 Undo errornous commit of Statespace change
2009-09-23 hoelzl 2009-09-23 correct variable order in approximate-method
2009-09-23 paulson 2009-09-23 merged
2009-09-23 paulson 2009-09-23 Correct chasing of type variable instantiations during type unification. The following theory should not raise exception TERM: constdefs somepredicate :: "(('b => 'b) => ('a => 'a)) => 'a => 'b => bool" "somepredicate upd v x == True" lemma somepredicate_idI: "somepredicate id (f v) v" by (simp add: somepredicate_def) lemma somepredicate_triv: "somepredicate upd v x ==> somepredicate upd v x" by assumption lemmas somepredicate_triv [OF somepredicate_idI] lemmas st' = somepredicate_triv[where v="h :: nat => bool"] lemmas st2 = st'[OF somepredicate_idI]
2009-09-23 haftmann 2009-09-23 hide newly introduced constants
2009-09-22 Philipp Meyer 2009-09-22 used standard fold function and type aliases
2009-09-21 Philipp Meyer 2009-09-21 sos method generates and uses proof certificates
2009-09-22 wenzelm 2009-09-22 full reserve of worker threads -- for improved CPU utilization;
2009-09-22 haftmann 2009-09-22 merged
2009-09-22 haftmann 2009-09-22 be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
2009-09-22 krauss 2009-09-22 tail -n 20: more helpful output if make fails
2009-09-22 haftmann 2009-09-22 corrected order of type variables in code equations; more precise certificate for cases
2009-09-21 Christian Urban 2009-09-21 merged
2009-09-21 Christian Urban 2009-09-21 tuned some proofs
2009-09-21 haftmann 2009-09-21 merged
2009-09-21 haftmann 2009-09-21 added session theory for Bali and Nominal_Examples
2009-09-21 haftmann 2009-09-21 added session theory for Nominal_Examples
2009-09-21 haftmann 2009-09-21 added session theory for Bali
2009-09-21 haftmann 2009-09-21 adjusted to new Number Theory scenario
2009-09-21 haftmann 2009-09-21 added session entry point theories
2009-09-21 haftmann 2009-09-21 common base for protocols with symmetric keys