isabelle: Graph

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