isabelle: Graph

simplify fixrec pattern match function
2010-10-19, by huffman
simplify some proofs
2010-10-17, by huffman
tuned
2010-10-19, by Christian Urban
added some facts about factorial and dvd, div and mod
2010-10-19, by bulwahn
removing something that probably slipped into the Quotient_List theory
2010-10-19, by bulwahn
Quotient package: partial equivalence introduction
2010-10-19, by Cezary Kaliszyk
reorganisation of the FSet theory (changed the primary naming scheme of constants and theorems to *_fset)
2010-10-18, by Christian Urban
remove dead code
2010-10-16, by huffman
remove old uses of 'simp_tac HOLCF_ss'
2010-10-16, by huffman
merged
2010-10-16, by huffman
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
2010-10-16, by huffman
reimplement proof automation for coinduct rules
2010-10-16, by huffman
add functions mk_imp, mk_all
2010-10-16, by huffman
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
2010-10-15, by huffman
simplify automation of induct proof
2010-10-15, by huffman
add function mk_adm
2010-10-15, by huffman
rewrite proof automation for finite_ind; get rid of case_UU_tac
2010-10-15, by huffman
put constructor argument specs in constr_info type
2010-10-14, by huffman
avoid using Global_Theory.get_thm
2010-10-14, by huffman
include iso_info as part of constr_info type
2010-10-14, by huffman
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
2010-10-14, by huffman
add take_strict_thms field to take_info type
2010-10-14, by huffman
add record type synonym 'constr_info'
2010-10-14, by huffman
add function take_theorems
2010-10-14, by huffman
add type annotation to avoid warning
2010-10-14, by huffman
cleaned up Fun_Cpo.thy; deprecated a few theorem names
2010-10-13, by huffman
edit comments
2010-10-13, by huffman
remove unneeded lemmas Lift_exhaust, Lift_cases
2010-10-12, by huffman
move lemmas from Lift.thy to Cfun.thy
2010-10-12, by huffman
cleaned up Adm.thy
2010-10-12, by huffman
remove unneeded lemmas from Fun_Cpo.thy
2010-10-12, by huffman
remove unused lemmas
2010-10-12, by huffman
reformulate lemma cont2cont_lub and move to Cont.thy
2010-10-12, by huffman
remove unused lemmas cont_fst_snd_D1, cont_fst_snd_D2
2010-10-12, by huffman
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
2010-10-11, by huffman
rename Ffun.thy to Fun_Cpo.thy
2010-10-11, by huffman
remove unused constant 'directed'
2010-10-11, by huffman
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
2010-10-11, by huffman
merged
2010-10-15, by paulson
prevention of self-referential type environments
2010-10-15, by paulson
FSet: definition changes propagated from Nominal and more use of 'descending' tactic
2010-10-15, by Cezary Kaliszyk
FSet tuned
2010-10-15, by Cezary Kaliszyk
FSet: give names to respectfulness theorems, rename list_all2_refl to avoid clash
2010-10-15, by Cezary Kaliszyk
NEWS
2010-10-14, by krauss
removed output syntax "'a ~=> 'b" for "'a => 'b option"
2010-10-10, by krauss
reactivated
2010-10-13, by krauss
slightly more robust proof
2010-10-12, by krauss
renamed type and constant 'sfp' to 'defl'; replaced syntax SFP('a) with DEFL('a)
2010-10-11, by huffman
merged
2010-10-11, by huffman
move all bifinite class instances to Bifinite.thy
2010-10-09, by huffman
rename class 'sfp' to 'bifinite'
2010-10-08, by huffman
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
2010-10-07, by huffman
add lemma typedef_ideal_completion
2010-10-07, by huffman
remove unused lemmas
2010-10-07, by huffman
remove Infinite_Set from ROOT.ML
2010-10-07, by huffman
remove some junk that made it in by accient
2010-10-07, by huffman
"setup" in theory
2010-10-11, by blanchet
added "trace_meson" configuration option, replacing old-fashioned reference
2010-10-11, by blanchet
added "trace_metis" configuration option, replacing old-fashioned references
2010-10-11, by blanchet
do not mention unqualified names, now that 'global' and 'local' are gone
2010-10-10, by krauss
simplified proof
2010-10-10, by nipkow
avoid generating several formulas with the same name ("tfrees")
2010-10-10, by blanchet
major reorganization/simplification of HOLCF type classes:
2010-10-06, by huffman
add lemma finite_deflation_intro
2010-10-05, by Brian Huffman
add lemmas finite_deflation_imp_compact, cast_below_cast_iff
2010-10-05, by Brian Huffman
move lemmas to Deflation.thy
2010-10-05, by Brian Huffman
simplify proofs of powerdomain inequalities
2010-10-05, by Brian Huffman
new lemmas about lub
2010-10-04, by huffman
define is_ub predicate using bounded quantifier
2010-10-04, by huffman
minimize theory imports
2010-10-02, by huffman
added lemmas to List_Cpo.thy
2010-10-01, by huffman
new_domain emits proper error message when a constructor argument type does not have sort 'rep'
2010-09-30, by huffman
move code from "Metis_Tactics" to "Metis_Reconstruct"
2010-10-06, by blanchet
merged
2010-10-06, by blanchet
qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
2010-10-06, by blanchet
get rid of function that duplicates existing Pure functionality
2010-10-06, by blanchet
remove needless fact
2010-10-06, by blanchet
added a few FIXMEs
2010-10-06, by blanchet
tuned comments
2010-10-05, by blanchet
document latest changes to Meson/Metis/Sledgehammer
2010-10-05, by blanchet
remove needless Metis facts
2010-10-05, by blanchet
hide one more name
2010-10-05, by blanchet
qualify names
2010-10-05, by blanchet
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
2010-10-05, by blanchet
clean up debugging output
2010-10-05, by blanchet
factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure
2010-10-05, by blanchet
got rid of overkill "meson_choice" attribute;
2010-10-05, by blanchet
more explicit name
2010-10-05, by blanchet
factor out "Meson_Tactic" from "Meson_Clausify"
2010-10-05, by blanchet
tuning
2010-10-04, by blanchet
move Metis into Plain
2010-10-04, by blanchet
added "Meson" theory to Makefile
2010-10-04, by blanchet
update authors
2010-10-04, by blanchet
remove Meson from Hilbert_Choice
2010-10-04, by blanchet
remove Meson from Sledgehammer
2010-10-04, by blanchet
move Meson to Plain
2010-10-04, by blanchet
move MESON files together
2010-10-04, by blanchet
paramify new skolems just like old ones (cf. reveal_old_skolem_terms)
2010-10-04, by blanchet
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
2010-10-04, by blanchet
correctly handle multiple copies of the same axiom with the same types
2010-10-04, by blanchet
put two operations in the right order
2010-10-04, by blanchet
reintroduce old "unify_prem_with_concl" code to avoid reaching unification bound + primitive handling for polymorphism
2010-10-04, by blanchet
apply "assume_tac" directly on the right assumption, using "rotate_tac" -- this ensures that the desired unifications are performed
2010-10-04, by blanchet
instantiate foralls and release exists in the order described by the topological order
2010-10-04, by blanchet
reverted 0bfaaa81fc62, since "Thm.rename_boundvars" can't be relied upon to give unique names to bound variables
2010-10-04, by blanchet
renamed internal function
2010-10-04, by blanchet
hack in MESON to make it less likely that variables (e.g. "x") get renamed (e.g. "xa") when resolving
2010-10-04, by blanchet
tuned header
2010-10-06, by haftmann
tuned
2010-10-05, by krauss
force less agressively
2010-10-05, by krauss
lexicographic_order: replace parallel map with laziness to avoid wasting cycles on proofs that are not needed
2010-10-05, by krauss
removed complicated (and rarely helpful) error reporting
2010-10-05, by krauss
discontinued continuations to simplify control flow; dropped optimization in scnp
2010-10-05, by krauss
use Cache structure instead of passing tables around explicitly
2010-10-05, by krauss
merged
2010-10-05, by haftmann
lemmas fold_commute and fold_commute_apply
2010-10-05, by haftmann
spelling
2010-05-07, by krauss
adjusted to inductive characterization of sorted
2010-10-04, by haftmann
tuned whitespace
2010-10-04, by haftmann
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
2010-10-04, by haftmann
turned distinct and sorted into inductive predicates: yields nice induction principles for free
2010-10-04, by haftmann
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
2010-10-04, by haftmann
some Poly/ML-specific debugging code escaped in the wild -- comment it out
2010-10-02, by blanchet
merged
2010-10-01, by haftmann
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
2010-10-01, by haftmann
moved ML_Context.value to Code_Runtime
2010-10-01, by haftmann
constant `contents` renamed to `the_elem`
2010-10-01, by haftmann
merged
2010-10-01, by blanchet
tune whitespace
2010-10-01, by blanchet
rename bound variables after skolemizing, if the axiom of choice is available
2010-10-01, by blanchet
tuning
2010-10-01, by blanchet
rename quantified variables earlier in the new skolemizer, to ensure consistent naming later (in the absence of the choice axiom)
2010-10-01, by blanchet
tune bound names
2010-10-01, by blanchet
merged
2010-10-01, by blanchet
avoid dependency on "int"
2010-10-01, by blanchet
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
2010-10-01, by blanchet
added "meson_choice" attribute as a step towards making (less powerful versions of) Meson/Metis/Sledgehammer work without the axiom of choice
2010-10-01, by blanchet
compute quantifier dependency graph in new skolemizer
2010-10-01, by blanchet
tuning
2010-10-01, by blanchet
compute substitutions in new skolemizer
2010-10-01, by blanchet
encode axiom number and cluster number in all zapped quantifiers to help discharging new skolemizer assumptions
2010-09-30, by blanchet
reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer
2010-09-30, by blanchet
encode number of skolem assumptions in them, for more efficient retrieval later
2010-09-30, by blanchet
move functions closer to where they're used
2010-09-30, by blanchet
Skolemizer tweaking
2010-09-30, by blanchet
"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
2010-09-29, by blanchet
finished renaming file and module
2010-09-29, by blanchet
rename file
2010-09-29, by blanchet
ignore Skolem assumption (if any)
2010-09-29, by blanchet
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
2010-09-29, by blanchet
first step towards a new skolemizer that doesn't require "Eps"
2010-09-29, by blanchet
cumulative update of generated files (since bf164c153d10);
2010-10-22, by wenzelm
removed ML_old.thy, which is largely superseded by ML.thy;
2010-10-22, by wenzelm
more on "Canonical argument order";
2010-10-22, by wenzelm
cover @{Isar.state};
2010-10-22, by wenzelm
more on "Style and orthography";
2010-10-22, by wenzelm
more on "Naming conventions";
2010-10-22, by wenzelm
tuned;
2010-10-22, by wenzelm
more on "Style and orthography";
2010-10-21, by wenzelm
more refs;
2010-10-21, by wenzelm
preliminary material on "Concrete syntax and type-checking";
2010-10-21, by wenzelm
more on "Association lists", based on more succinct version of older material;
2010-10-20, by wenzelm
clarified "lists as a set-like container";
2010-10-20, by wenzelm
more robust treatment of "op IDENT";
2010-10-19, by wenzelm
more on messages;
2010-10-19, by wenzelm
more on synchronized variables;
2010-10-19, by wenzelm
tuned;
2010-10-19, by wenzelm
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
2010-10-19, by wenzelm
misc tuning;
2010-10-19, by wenzelm
somewhat modernized version of "Thread-safe programming";
2010-10-18, by wenzelm
more robust examples: explicit @{assert} instead of unchecked output;
2010-10-18, by wenzelm
more on "Configuration options";
2010-10-18, by wenzelm
tuned;
2010-10-18, by wenzelm
more on "Basic data types";
2010-10-18, by wenzelm
more on "Integers";
2010-10-17, by wenzelm
use continental paragraph style, which works better with mixture of (in)formal text;
2010-10-17, by wenzelm
robustified "warn" environment if \parindent is zero (e.g. within itemize, description etc.);
2010-10-17, by wenzelm
more on "Basic ML data types";
2010-10-16, by wenzelm
more robust treatment of symbolic indentifiers (which may contain colons);
2010-10-16, by wenzelm
more examples;
2010-10-16, by wenzelm
tuned;
2010-10-16, by wenzelm
more on "Exceptions";
2010-10-16, by wenzelm
more on "Exceptions";
2010-10-15, by wenzelm
more examples;
2010-10-15, by wenzelm
tuned chapter arrangement;
2010-10-15, by wenzelm
more examples;
2010-10-15, by wenzelm
moved bind_thm(s) to implementation manual;
2010-10-15, by wenzelm
more on "Attributes";
2010-10-14, by wenzelm
misc tuning and clarification;
2010-10-14, by wenzelm
more on "Proof methods";
2010-10-13, by wenzelm
examples in Isabelle/HOL;
2010-10-13, by wenzelm
more on Proof.theorem;
2010-10-13, by wenzelm
tuned;
2010-10-13, by wenzelm
more examples;
2010-10-12, by wenzelm
more on "Isar language elements";
2010-10-12, by wenzelm
more examples;
2010-10-11, by wenzelm
more refs;
2010-10-11, by wenzelm
misc tuning;
2010-10-11, by wenzelm
removed some obsolete reference material;
2010-10-10, by wenzelm
cover some more theory operations;
2010-10-10, by wenzelm
note on Isabelle file specifications;
2010-10-10, by wenzelm
modernized version of "Message output channels";
2010-10-10, by wenzelm
removed some really old reference material;
2010-10-10, by wenzelm
more examples;
2010-10-09, by wenzelm
various concrete ML antiquotations;
2010-10-09, by wenzelm
prefer checked antiquotations;
2010-10-09, by wenzelm
clarified tag markup;
2010-10-09, by wenzelm
more on ML antiquotations;
2010-10-08, by wenzelm
keep normal size for %mlref tag;
2010-10-08, by wenzelm
basic setup for ML antiquotations -- with rail diagrams;
2010-10-08, by wenzelm
eliminated "Toplevel control", which belongs to TTY/ProofGeneral model;
2010-10-08, by wenzelm
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
2010-10-08, by wenzelm
misc tuning;
2010-10-08, by wenzelm
more on Isabelle/ML;
2010-10-07, by wenzelm
basic setup for Chapter 0: Isabelle/ML;
2010-10-07, by wenzelm
minor tuning and updating;
2010-10-07, by wenzelm
made SML/NJ happy;
2010-10-01, by wenzelm
merged
2010-10-01, by wenzelm
use module integer for Eval
2010-10-01, by haftmann
check whole target hierarchy for existing reserved symbols
2010-10-01, by haftmann
added polyml_as_definition -- using external SML files as substitute for proper definitions -- only for polyml!
2010-10-01, by haftmann
tuned default "Prover Session" perspective;
2010-10-01, by wenzelm
eliminated ancient OldTerm.term_frees;
2010-10-01, by wenzelm
more antiquotations;
2010-10-01, by wenzelm
simplified outer syntax setup;
2010-10-01, by wenzelm
chop_while replace drop_while and take_while
2010-10-01, by haftmann
merged
2010-10-01, by haftmann
take_while, drop_while
2010-09-30, by haftmann
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
2010-09-30, by huffman
fixrec: rename match_cpair to match_Pair
2010-09-30, by huffman
remove code for obsolete 'fixpat' command
2010-09-15, by huffman
clean up definition of compile_pat function
2010-09-15, by huffman
rename some fixrec pattern-match compilation functions
2010-09-15, by huffman
adding example for case expressions
2010-09-30, by bulwahn
applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
2010-09-30, by bulwahn
merged
2010-09-30, by bulwahn
adapting manual configuration in examples
2010-09-30, by bulwahn
finding the counterexample with different options (manually limited precisely, manually limited global, automatically limited global)
2010-09-30, by bulwahn
adding option to globally limit the prolog execution
2010-09-30, by bulwahn
removing dead code
2010-09-30, by bulwahn
value uses bare compiler invocation: generated code does not contain antiquotations
2010-09-30, by haftmann
updated files to recent changes
2010-09-30, by haftmann
corrected subsumption check: arguments have been reversed; addition of default equations to non-default equations is identity
2010-09-30, by haftmann
tuned
2010-09-30, by haftmann
merged
2010-09-30, by haftmann
redundancy check: drop trailing Var arguments (avoids eta problems with equations)
2010-09-29, by haftmann
merged
2010-09-29, by wenzelm
removing obsolete distinction between prod_case and other case expressions after merging of split and prod_case (d3daea901123) in predicate compiler
2010-09-29, by bulwahn
merged
2010-09-29, by bulwahn
adding splitting of conjuncts in assumptions as forward rule on theorems; replacing term transformation for splitting conjuncts by theorem transformation; removing obsolete functions; tuned
2010-09-29, by bulwahn
added test case for predicate arguments in higher-order argument position
2010-09-29, by bulwahn
improving the compilation to handle predicate arguments in higher-order argument positions
2010-09-29, by bulwahn
added a test case to Predicate_Compile_Tests
2010-09-29, by bulwahn
putting the last step of the proof in a TRY block to handle the case that the simplifier already solved the goal
2010-09-29, by bulwahn
backed out my old attempt at single_hyp_subst_tac (67cd6ed76446)
2010-09-29, by krauss
scala is reserved identifier
2010-09-29, by haftmann
platform-sensitive contrib paths for ghc, ocaml
2010-09-29, by haftmann
fact listsum now names listsum_foldl
2010-09-29, by haftmann
delete code lemma explicitly
2010-09-29, by haftmann
moved old_primrec source to nominal package, where it is still used
2010-09-29, by haftmann
dropped old primrec package
2010-09-28, by haftmann
merged
2010-09-28, by haftmann
localized listsum
2010-09-28, by haftmann
lemma listsum_conv_fold
2010-09-28, by haftmann
merged
2010-09-28, by haftmann
NEWS
2010-09-28, by haftmann
dropped syntax for old primrec package
2010-09-28, by haftmann
modernized session
2010-09-28, by haftmann
merged
2010-09-28, by bulwahn
using SUBPROOF to ensure that rewriting is not done on the further subgoals of proof
2010-09-28, by bulwahn
avoiding instable rotate_tac and using the nice Subgoal.FOCUS_PREMS instead
2010-09-28, by bulwahn
adding test case for interpretation of arguments that are predicates simply as input
2010-09-28, by bulwahn
only modes but not types are used to destruct terms and types; this allows to interpret arguments that are predicates simply as input
2010-09-28, by bulwahn
weakening check for higher-order relations, but adding check for consistent modes
2010-09-28, by bulwahn
handling higher-order relations in output terms; improving proof procedure; added test case
2010-09-28, by bulwahn
renaming use_random to use_generators in the predicate compiler
2010-09-28, by bulwahn
fixed a typo that caused the preference of non-random modes to be ignored
2010-09-28, by bulwahn
merged
2010-09-28, by haftmann
modernized primrecs
2010-09-28, by haftmann
modernized session
2010-09-28, by haftmann
consolidated tupled_lambda; moved to structure HOLogic
2010-09-28, by krauss
added dependency to base image to ensure that the doc test actually rebuilds the tutorial
2010-09-28, by haftmann
no longer declare .psimps rules as [simp].
2010-09-28, by krauss
added dependency to base images to ensure that the doc test actually rebuilds the tutorials
2010-09-28, by krauss
removed unnecessary reference poking (cf. f45d332a90e3)
2010-09-28, by krauss
merged
2010-09-28, by haftmann
consider quick_and_dirty option before loading theory
2010-09-28, by haftmann
dropped obsolete mk_tcl
2010-09-28, by krauss
make SML/NJ happy
2010-09-28, by blanchet
merged
2010-09-27, by haftmann
combine quote and typewriter tag; typewriter considers isa@parindent
2010-09-27, by haftmann
combine quote and typewriter/tt tag
2010-09-27, by haftmann
combine quote and typewriter tag; typewriter considers isa@parindent
2010-09-27, by haftmann
combine quote and typewriter tag
2010-09-27, by haftmann
CONTROL-mouse management: handle windowDeactivated as well;
2010-09-29, by wenzelm
CONTROL-mouse management: handle windowIconified;
2010-09-28, by wenzelm
basic support for message popups via HTML_Panel;
2010-09-28, by wenzelm
tuned default perspective;
2010-09-28, by wenzelm
tuned README;
2010-09-28, by wenzelm
more defensive overview.paintComponent: avoid potential crash due to buffer change while painting;
2010-09-28, by wenzelm
tuned README;
2010-09-28, by wenzelm
more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state;
2010-09-28, by wenzelm
moved "auto-start" to options panel;
2010-09-27, by wenzelm
renamed raw output primitives to emphasize their meaning -- not to be used in user-space;
2010-09-27, by wenzelm
added Standard_System.unzip (for platform file-system);
2010-09-27, by wenzelm
bulk read: observe EOF protocol more carefully -- 0 counts as successful read;
2010-09-27, by wenzelm
tuned whitespace;
2010-09-27, by wenzelm
merged
2010-09-27, by wenzelm
lemma remdups_map_remdups
2010-09-27, by haftmann
lemma remdups_list_of_dlist
2010-09-27, by haftmann
merged
2010-09-27, by bulwahn
adopting example
2010-09-27, by bulwahn
adding further tracing messages; tuned
2010-09-27, by bulwahn
handling nested cases more elegant by requiring less new constants
2010-09-27, by bulwahn
merged
2010-09-27, by blanchet
renamed function
2010-09-27, by blanchet
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
2010-09-27, by blanchet
comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
2010-09-27, by blanchet
remove needless flag
2010-09-27, by blanchet
added hint on reference equality
2010-09-27, by haftmann
treat equality on refs and arrays as primitive operation
2010-09-27, by haftmann
corrected OCaml operator precedence
2010-09-27, by haftmann
corrected scope of closure
2010-09-27, by haftmann
merged
2010-09-27, by haftmann
separate quote tag from tt tag
2010-09-27, by haftmann
separate quote tag from tt tag
2010-09-24, by haftmann
make SML/NJ happy
2010-09-25, by blanchet
some more options to robustify posix_untar;
2010-09-27, by wenzelm
more efficient posix_untar -- avoid really slow java.util.zip.GZIPInputStream;
2010-09-27, by wenzelm
back to UseQuartz=true -- used to be default on Apple Java 1.5;
2010-09-27, by wenzelm
raw_untar.raw_execute with native cwd, to avoid cross-platform complications;
2010-09-26, by wenzelm
added Standard_System.raw_untar;
2010-09-26, by wenzelm
some markup for inner syntax tokens;
2010-09-26, by wenzelm
tuned signatures and messages;
2010-09-26, by wenzelm
Session_Dockable: more startup controls;
2010-09-25, by wenzelm
simplified / clarified Session.Phase;
2010-09-25, by wenzelm
more precise treatment of backgrounds vs. rectangles;
2010-09-25, by wenzelm
tuned mk_fifo;
2010-09-25, by wenzelm
tuned signature;
2010-09-25, by wenzelm
tuned border;
2010-09-24, by wenzelm
more informative Session.Phase;
2010-09-24, by wenzelm
merged
2010-09-24, by wenzelm
merged
2010-09-24, by haftmann
tuned schema table
2010-09-24, by haftmann
tuned warning_color;
2010-09-24, by wenzelm
tuned error_color;
2010-09-24, by wenzelm
some attempts to improve visual appearance of bad text;
2010-09-24, by wenzelm
clarified @{type} antiquotation: abbreviations and nonterminals count as "syntactic", disallow TFrees;
2010-09-24, by wenzelm
updated generated file;
2010-09-24, by wenzelm
modernized structure Ord_List;
2010-09-24, by wenzelm
isatest: indicate Isabelle version;
2010-09-24, by wenzelm
actually handle Type.TYPE_MATCH, not arbitrary exceptions;
2010-09-24, by wenzelm
merged
2010-09-24, by wenzelm
prefer typewrite tag over raw latex environment
2010-09-24, by haftmann
avoid fragile tranclp syntax; corrected resolution; corrected typo
2010-09-24, by haftmann
merged
2010-09-24, by wenzelm
use typewriter tag instead of bare environment
2010-09-24, by haftmann
dropped dead code
2010-09-24, by haftmann
always add trailing newline for presentation
2010-09-24, by haftmann
corrected omission
2010-09-24, by haftmann
fixed small font size fore typewriter text
2010-09-24, by haftmann
merged
2010-09-24, by haftmann
load theory explicitly
2010-09-24, by haftmann
merge
2010-09-24, by blanchet
make SML/NJ happier -- temporary solution until Metis is fixed upstream
2010-09-24, by blanchet
merged
2010-09-24, by bulwahn
being a little less strict than in 2e06dad03dd3
2010-09-24, by bulwahn
quotient package: respectfulness and preservation of identity.
2010-09-24, by Cezary Kaliszyk
merged
2010-09-23, by haftmann
merged
2010-09-23, by haftmann
removed superfluous output_typewriter from cs 65064e8f269
2010-09-23, by haftmann
more idiomatic handling of latex typewriter type setting
2010-09-23, by haftmann
more canonical type setting of type writer code examples
2010-09-23, by haftmann
resynchronize isabelle.sty
2010-09-23, by haftmann
reverted cs 5aced2f43837 -- no need for hardwired latex command here
2010-09-23, by haftmann
reverted cs 07549694e2f1 -- use re-printing with current print mode instead after code assembly, avoid Latex.output_typewriter
2010-09-23, by haftmann
reverted cs 07549694e2f1
2010-09-23, by haftmann
shifted abstraction over imperative print mode
2010-09-23, by haftmann
removing unneccessary expansion procedure for elimination rules; removing obsolete elim preprocessing; tuned
2010-09-23, by bulwahn
moving the preprocessing of introduction rules after the code_pred command; added tuple expansion preprocessing of elimination rule
2010-09-23, by bulwahn
exporting the generic version instead of the context version in quickcheck
2010-09-23, by bulwahn
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
2010-09-23, by bulwahn
adding a mutual recursive example for named alternative rules for the predicate compiler
2010-09-23, by bulwahn
handling TYPE_MATCH error by raising user error message if user gives introduction rules with mismatching types
2010-09-23, by bulwahn
improving naming of assumptions in code_pred
2010-09-23, by bulwahn
adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
2010-09-23, by bulwahn
handling equivalences smarter in the predicate compiler
2010-09-23, by bulwahn
removing duplicate rewrite rule from simpset in predicate compiler
2010-09-23, by bulwahn
rewriting function mk_Eval_of in predicate compiler
2010-09-23, by bulwahn
merged
2010-09-23, by haftmann
improved and tuned external codegen tool
2010-09-23, by haftmann
make SML/NJ happy
2010-09-23, by blanchet
CONTRIBUTORS and NEWS
2010-09-23, by haftmann
corrections and tuning
2010-09-23, by haftmann
merged
2010-09-22, by haftmann
merged
2010-09-22, by haftmann
merged
2010-09-22, by haftmann
tuned
2010-09-22, by haftmann
persistent session-panel.selection;
2010-09-24, by wenzelm
slightly more robust EditBus plumbing wrt. Document_View/Document_Model;
2010-09-24, by wenzelm
permissive exit;
2010-09-24, by wenzelm
added Session_Dockable.session_phase label;
2010-09-24, by wenzelm
separate Plugin.init_model;
2010-09-23, by wenzelm
simplified Session.Phase;
2010-09-23, by wenzelm
tuned messages -- cf. Admin/MacOS/App1;
2010-09-23, by wenzelm
tuned dialog;
2010-09-23, by wenzelm
explicit Session.Phase indication with associated event bus;
2010-09-23, by wenzelm
tuned signature;
2010-09-23, by wenzelm
Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;
2010-09-23, by wenzelm
tuned;
2010-09-23, by wenzelm
manage persistent syslog via Session, not Isabelle_Process;
2010-09-23, by wenzelm
tuned prover message categorization;
2010-09-23, by wenzelm
tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
2010-09-23, by wenzelm
tuned message;
2010-09-23, by wenzelm
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
2010-09-22, by wenzelm
Snapshot.convert/revert: explicit error report to isolate sporadic crash;
2010-09-22, by wenzelm
make compiler doubly sure;
2010-09-22, by wenzelm
isabelle-process: less verbose no-commit mode;
2010-09-22, by wenzelm
tuned message;
2010-09-22, by wenzelm
tuned panel names and actions;
2010-09-22, by wenzelm
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
2010-09-22, by wenzelm
reactivated polyml-5.4.0 -- SVN 1214 fixes a problem with arbitrary precision arithmetic that was triggered by method "approximation" in HOL/Decision_Procs/Approximation_Ex.thy;
2010-09-22, by wenzelm
merged
2010-09-22, by nipkow
more lists lemmas
2010-09-22, by nipkow
merged
2010-09-22, by wenzelm
merged
2010-09-22, by haftmann
tuned text
2010-09-22, by haftmann
sections on @{code} and code_reflect
2010-09-22, by haftmann
formal syntax diagram for code_reflect
2010-09-22, by haftmann
distinguish SML and Eval explicitly
2010-09-22, by haftmann
no_frees_* is subsumed by new framework mechanisms in Code_Preproc
2010-09-21, by haftmann
reject term variables explicitly
2010-09-21, by haftmann
avoid frees and vars in terms to be evaluated by abstracting and applying
2010-09-21, by haftmann
tuned whitespace
2010-09-21, by haftmann
make SML/NJ happier
2010-09-22, by blanchet
more conventional conversion signature
2010-09-21, by haftmann
added nbe paper
2010-09-21, by haftmann
continued section abut evaluation
2010-09-21, by haftmann
make SML/NJ happier
2010-09-21, by blanchet
new lemma
2010-09-21, by nipkow
merged
2010-09-20, by nipkow
new lemmas
2010-09-20, by nipkow
revert b96941dddd04 and c13b4589fddf, which dramatically inflate proof terms
2010-09-20, by blanchet
basic setup for Session_Dockable controls;
2010-09-22, by wenzelm
tuned signature;
2010-09-22, by wenzelm
more content for Session_Dockable;
2010-09-22, by wenzelm
basic support for full document rendering;
2010-09-22, by wenzelm
Session_Dockable: basic syslog output;
2010-09-22, by wenzelm
just one Session.raw_messages event bus;
2010-09-22, by wenzelm
more reactive handling of Isabelle_Process startup errors;
2010-09-22, by wenzelm
eliminated Simple_Thread shorthands that can overlap with full version;
2010-09-22, by wenzelm
main Isabelle_Process via Isabelle_System.Managed_Process;
2010-09-22, by wenzelm
more robust Managed_Process.kill: check after sending signal;
2010-09-22, by wenzelm
more robust lib/scripts/process, with explicit script/no_script mode;
2010-09-22, by wenzelm
Standard_System.with_tmp_file: deleteOnExit to make double sure;
2010-09-22, by wenzelm
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
2010-09-21, by wenzelm
tuned whitespace;
2010-09-21, by wenzelm
tuned;
2010-09-21, by wenzelm
added Standard_System.slurp convenience;
2010-09-21, by wenzelm
added Simple_Thread.future convenience;
2010-09-21, by wenzelm
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
2010-09-20, by wenzelm
tuned;
2010-09-20, by wenzelm
more robust Isabelle_System.rm_fifo: avoid external bash invocation, which might not work in JVM shutdown phase (due to Runtime.addShutdownHook);
2010-09-20, by wenzelm
tuned;
2010-09-20, by wenzelm
added Isabelle_Process.syslog;
2010-09-20, by wenzelm
updated keywords;
2010-09-20, by wenzelm
merged
2010-09-20, by wenzelm
merged
2010-09-20, by haftmann
corrected long-overlooked slip: the Pure equality of a code equation is no part of the code equation itself
2010-09-20, by haftmann
dynamic_eval_conv static_eval_conv: certification of previously unreliably reconstructed evaluated term
2010-09-20, by haftmann
Pure equality is a regular cpde operation
2010-09-20, by haftmann
full palette of dynamic/static value(_strict/exn)
2010-09-20, by haftmann
Factored out ML into separate file
2010-09-20, by haftmann
merged
2010-09-20, by wenzelm
merged
2010-09-20, by blanchet
remove needless exception
2010-09-20, by blanchet
preprocess "Ex" before doing clausification in Metis;
2010-09-20, by blanchet
expand_fun_eq -> fun_eq_iff
2010-09-20, by haftmann
use buffers instead of string concatenation
2010-09-20, by haftmann
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-20, by wenzelm