krauss [Thu, 24 Mar 2011 16:39:37 +0100] rev 42095
added more judgement day provers
bulwahn [Thu, 24 Mar 2011 15:29:31 +0100] rev 42094
allowing special set comprehensions in values command; adding an example for special set comprehension in values
bulwahn [Thu, 24 Mar 2011 10:39:47 +0100] rev 42093
merged
bulwahn [Wed, 23 Mar 2011 08:50:42 +0100] rev 42092
adding documentation about the eval option in quickcheck
bulwahn [Wed, 23 Mar 2011 08:50:40 +0100] rev 42091
adapting Quickcheck_Prolog to latest changes
bulwahn [Wed, 23 Mar 2011 08:50:39 +0100] rev 42090
changing Quickcheck_Narrowing's main function to enumerate the depth instead upto the depth
bulwahn [Wed, 23 Mar 2011 08:50:32 +0100] rev 42089
adapting mutabelle; exporting more Quickcheck functions
bulwahn [Wed, 23 Mar 2011 08:50:31 +0100] rev 42088
making quickcheck's result value more formal; allowing more result information to be returned after timeout; adding output of timing information in quickcheck
bulwahn [Wed, 23 Mar 2011 08:50:29 +0100] rev 42087
changing timeout behaviour of quickcheck to proceed after command rather than failing; adding a test case for timeout
wenzelm [Sat, 26 Mar 2011 12:01:40 +0100] rev 42086
added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
recovered printing of Hoare assign statements from 45d090186bbe;
wenzelm [Sat, 26 Mar 2011 10:52:29 +0100] rev 42085
tuned;
wenzelm [Sat, 26 Mar 2011 10:25:17 +0100] rev 42084
dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;
wenzelm [Thu, 24 Mar 2011 16:56:19 +0100] rev 42083
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm [Thu, 24 Mar 2011 16:47:24 +0100] rev 42082
more direct loose_bvar1;
tuned;
wenzelm [Thu, 24 Mar 2011 13:54:39 +0100] rev 42081
indentation;
wenzelm [Thu, 24 Mar 2011 11:45:39 +0100] rev 42080
update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm [Wed, 23 Mar 2011 21:07:05 +0100] rev 42079
added editor mode line;
wenzelm [Wed, 23 Mar 2011 20:57:37 +0100] rev 42078
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
qualified Proofterm.proofs to facilitate grepping;
wenzelm [Wed, 23 Mar 2011 20:51:36 +0100] rev 42077
list Isabelle tools via perl script, which is much faster that bash plumbing, especially on Cygwin;
exclude backup files;
boehmes [Wed, 23 Mar 2011 16:42:09 +0100] rev 42076
updated contributed components
boehmes [Wed, 23 Mar 2011 15:33:17 +0100] rev 42075
Z3 non-commercial usage may explicitly be declined
boehmes [Wed, 23 Mar 2011 14:29:29 +0100] rev 42074
export status function to query whether Z3 has been activated for usage within Isabelle
blanchet [Wed, 23 Mar 2011 10:38:50 +0100] rev 42073
merge
blanchet [Wed, 23 Mar 2011 10:18:42 +0100] rev 42072
avoid illegal variable names, which then yield "Not an identifier" errors in "rename_tac"
blanchet [Wed, 23 Mar 2011 10:06:27 +0100] rev 42071
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
default to "e" rather than "vampire" since E is part of the Isabelle bundle
boehmes [Wed, 23 Mar 2011 10:21:29 +0100] rev 42070
really be quiet
krauss [Wed, 23 Mar 2011 09:15:49 +0100] rev 42069
replace hardwired MIRABELLE_OUTPUT_PATH by temporary directory derived from ISABELLE_TMP_PREFIX and $$ -- old behaviour can be achieved by manually setting MIRABELLE_OUTPUT_PATH
wenzelm [Tue, 22 Mar 2011 21:22:50 +0100] rev 42068
merged
hoelzl [Tue, 22 Mar 2011 20:06:10 +0100] rev 42067
standardized headers
hoelzl [Tue, 22 Mar 2011 18:53:05 +0100] rev 42066
generalized Caratheodory from algebra to ring_of_sets