| Thu, 01 Sep 2005 22:15:12 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:40 +0200 |
wenzelm |
refer to theory instead of low-level tsig;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 11:16:34 +0200 |
haftmann |
(intermediate commit)
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:13:59 +0200 |
wenzelm |
get_thm(s): Name;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:35:27 +0200 |
wenzelm |
accomodate change of TheoryDataFun;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2005 12:03:22 +0200 |
wenzelm |
NameSpace.extern_table;
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:19 +0200 |
wenzelm |
Sign.declare_name replaces NameSpace.extend;
|
file |
diff |
annotate
|
| Wed, 25 May 2005 10:18:09 +0200 |
kleing |
removed obsolete findI, findE, findEs
|
file |
diff |
annotate
|
| Sun, 22 May 2005 16:51:09 +0200 |
wenzelm |
findI/Es/E: adapted to FindTheorems.find_XXX, results use thmref instead of string;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 22:02:06 +0200 |
wenzelm |
superceded by Pure.thy and CPure.thy;
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 17:59:48 +0100 |
berghofe |
Adapted to modified interface of PureThy.get_thm(s).
|
file |
diff |
annotate
|
| Wed, 09 Jun 2004 18:53:13 +0200 |
wenzelm |
Syntax.default_mode;
|
file |
diff |
annotate
|
| Sat, 29 May 2004 15:01:36 +0200 |
wenzelm |
Output.timing;
|
file |
diff |
annotate
|
| Thu, 22 Apr 2004 10:52:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 03 Feb 2003 11:04:16 +0100 |
berghofe |
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
|
file |
diff |
annotate
|
| Wed, 13 Nov 2002 15:34:35 +0100 |
berghofe |
Added simple_prove_goal_cterm.
|
file |
diff |
annotate
|
| Mon, 21 Oct 2002 17:07:58 +0200 |
berghofe |
Changed type of Logic.strip_horn.
|
file |
diff |
annotate
|
| Mon, 14 Oct 2002 10:44:32 +0200 |
nipkow |
Ported find_intro/elim to Isar.
|
file |
diff |
annotate
|
| Tue, 02 Jul 2002 15:37:49 +0200 |
wenzelm |
emulate old thms_containing;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2001 00:46:26 +0100 |
wenzelm |
theory data: removed obsolete finish method;
|
file |
diff |
annotate
|
| Fri, 09 Nov 2001 00:19:20 +0100 |
wenzelm |
theory data: finish method;
|
file |
diff |
annotate
|
| Thu, 01 Nov 2001 21:09:53 +0100 |
wenzelm |
parking code for old-style locales here;
|
file |
diff |
annotate
|
| Sat, 27 Oct 2001 00:09:59 +0200 |
wenzelm |
impose hyps on initial goal configuration (prevents res_inst_tac problems);
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 18:01:15 +0200 |
wenzelm |
make this module appeat late in Pure;
|
file |
diff |
annotate
|
| Wed, 12 Sep 2001 18:10:52 +0200 |
wenzelm |
result_error_default: include msg;
|
file |
diff |
annotate
|
| Sat, 08 Sep 2001 20:05:14 +0200 |
wenzelm |
result_error_default: output *single* error message;
|
file |
diff |
annotate
|
| Fri, 29 Dec 2000 19:43:52 +0100 |
wenzelm |
proper error msg;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2000 18:50:52 +0100 |
wenzelm |
check result: Envir.beta_norm;
|
file |
diff |
annotate
|
| Thu, 10 Aug 2000 11:33:40 +0200 |
paulson |
the "nocheck" versions of goal functions now standardize their result
|
file |
diff |
annotate
|
| Fri, 04 Aug 2000 22:58:38 +0200 |
wenzelm |
Term.no_dummy_patterns;
|
file |
diff |
annotate
|
| Tue, 30 May 2000 16:03:09 +0200 |
wenzelm |
global timing flag;
|
file |
diff |
annotate
|
| Thu, 18 May 2000 18:46:13 +0200 |
wenzelm |
added disable_pr, enable_pr;
|
file |
diff |
annotate
|
| Wed, 05 Jan 2000 11:35:18 +0100 |
wenzelm |
TypeInfer.logicT;
|
file |
diff |
annotate
|
| Wed, 27 Oct 1999 11:12:10 +0200 |
oheimb |
reset_goals no longer empties the proof stack
|
file |
diff |
annotate
|
| Wed, 29 Sep 1999 13:51:23 +0200 |
wenzelm |
use Drule.strip_shyps_warning;
|
file |
diff |
annotate
|
| Wed, 18 Aug 1999 20:40:28 +0200 |
wenzelm |
proper writeln of begin_state;
|
file |
diff |
annotate
|
| Tue, 17 Aug 1999 17:51:35 +0200 |
wenzelm |
reset_goals;
|
file |
diff |
annotate
|
| Thu, 22 Jul 1999 20:53:54 +0200 |
wenzelm |
avoid '(0 subgoals)';
|
file |
diff |
annotate
|
| Sat, 10 Jul 1999 21:35:08 +0200 |
wenzelm |
prove_goalw_cterm_general: pass exeption;
|
file |
diff |
annotate
|
| Wed, 07 Jul 1999 00:15:06 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:33:00 +0100 |
wenzelm |
qualify Theory.sign_of etc.;
|
file |
diff |
annotate
|
| Wed, 03 Feb 1999 16:45:45 +0100 |
wenzelm |
added Goal(w) and Export (from context.ML);
|
file |
diff |
annotate
|
| Fri, 15 Jan 1999 16:13:31 +0100 |
oheimb |
removed empty line (in case of empty begin_state marker) before Level line
|
file |
diff |
annotate
|
| Fri, 04 Dec 1998 10:45:20 +0100 |
paulson |
better export for nested locales
|
file |
diff |
annotate
|
| Wed, 25 Nov 1998 13:57:17 +0100 |
wenzelm |
removed redirect_to_latex stuff;
|
file |
diff |
annotate
|
| Thu, 29 Oct 1998 14:32:43 +0100 |
wenzelm |
tuned current_goals_markers semantics to avoid empty lines;
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 18:48:25 +0200 |
paulson |
better reporting of "Additional hypotheses" in a locale
|
file |
diff |
annotate
|
| Thu, 22 Oct 1998 20:07:42 +0200 |
wenzelm |
support current_goals_markers ref variable for print_current_goals;
|
file |
diff |
annotate
|
| Mon, 05 Oct 1998 10:31:43 +0200 |
paulson |
Now prove_goalw_cterm never prints timing statistics
|
file |
diff |
annotate
|
| Thu, 13 Aug 1998 17:43:00 +0200 |
paulson |
Rule mk_triv_goal for making instances of triv_goal
|
file |
diff |
annotate
|
| Tue, 04 Aug 1998 18:22:04 +0200 |
wenzelm |
added export: thm -> thm;
|
file |
diff |
annotate
|
| Mon, 29 Jun 1998 21:33:35 +0200 |
wenzelm |
moved actual (C)Pure theories to pure.ML;
|
file |
diff |
annotate
|
| Wed, 17 Jun 1998 10:48:38 +0200 |
nipkow |
Goals may now contain assumptions, which are not returned.
|
file |
diff |
annotate
|
| Fri, 05 Jun 1998 14:23:27 +0200 |
wenzelm |
tuned print_exn;
|
file |
diff |
annotate
|
| Sat, 22 Nov 1997 13:27:02 +0100 |
wenzelm |
fixed warning;
|
file |
diff |
annotate
|
| Fri, 21 Nov 1997 15:27:43 +0100 |
wenzelm |
changed Sequence interface (now Seq, in seq.ML);
|
file |
diff |
annotate
|
| Wed, 12 Nov 1997 16:21:26 +0100 |
wenzelm |
moved 'latex' from library.ML to goals.ML;
|
file |
diff |
annotate
|
| Fri, 24 Oct 1997 17:14:02 +0200 |
wenzelm |
Pure.thy;
|
file |
diff |
annotate
|
| Thu, 23 Oct 1997 12:10:55 +0200 |
wenzelm |
Sign.stamp_names_of;
|
file |
diff |
annotate
|
| Mon, 13 Oct 1997 17:47:59 +0200 |
wenzelm |
uses Sign.str_of_sort;
|
file |
diff |
annotate
|
| Thu, 25 Sep 1997 12:10:07 +0200 |
paulson |
Prints warnings using the "warning" function instead of "writeln"
|
file |
diff |
annotate
|
| Thu, 11 Sep 1997 16:16:03 +0200 |
wenzelm |
removed print_goals_ref (which was broken anyway);
|
file |
diff |
annotate
|
| Fri, 18 Jul 1997 14:06:54 +0200 |
wenzelm |
tuned error propagation msg;
|
file |
diff |
annotate
|
| Fri, 18 Jul 1997 13:52:35 +0200 |
wenzelm |
tuned warnings;
|
file |
diff |
annotate
|
| Wed, 16 Apr 1997 18:22:10 +0200 |
wenzelm |
Sorts.str_of_sort;
|
file |
diff |
annotate
|
| Wed, 02 Apr 1997 17:28:27 +0200 |
wenzelm |
changed signature of dummy goal from proto_pure to pure;
|
file |
diff |
annotate
|
| Tue, 04 Feb 1997 10:33:58 +0100 |
paulson |
Gradual switching to Basis Library functions nth, drop, etc.
|
file |
diff |
annotate
|
| Fri, 17 Jan 1997 11:13:18 +0100 |
paulson |
Added the prlim command
|
file |
diff |
annotate
|
| Fri, 08 Nov 1996 14:07:56 +0100 |
paulson |
Removed "standard" call from uresult, to allow specialist applications
|
file |
diff |
annotate
|
| Thu, 24 Oct 1996 10:42:42 +0200 |
paulson |
Allowing negative levels (as offsets) in prlev and choplev
|
file |
diff |
annotate
|
| Tue, 20 Aug 1996 12:40:17 +0200 |
paulson |
Added ref to allow suppression of error msgs
|
file |
diff |
annotate
|
| Thu, 28 Mar 1996 17:27:54 +0100 |
berghofe |
Added functions pr_latex and printgoal_latex which
|
file |
diff |
annotate
|
| Fri, 15 Mar 1996 12:01:19 +0100 |
berghofe |
Added some functions which allow redirection of Isabelle's output
|
file |
diff |
annotate
|
| Mon, 11 Mar 1996 14:13:36 +0100 |
paulson |
Made an exception handler more specific
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 12:19:47 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 14:16:13 +0100 |
clasohm |
inserted tabs again
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:56:41 +0100 |
clasohm |
removed tabs
|
file |
diff |
annotate
|
| Fri, 22 Dec 1995 10:26:57 +0100 |
paulson |
"prepare_proof" has been simplified because
|
file |
diff |
annotate
|
| Fri, 01 Sep 1995 13:16:24 +0200 |
wenzelm |
adapted to new version of shyps-stuff;
|
file |
diff |
annotate
|
| Tue, 01 Aug 1995 17:21:05 +0200 |
wenzelm |
modified prepare_proof to handle shyps;
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 11:48:05 +0100 |
clasohm |
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
|
file |
diff |
annotate
|
| Mon, 27 Feb 1995 18:07:59 +0100 |
lcp |
Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
|
file |
diff |
annotate
|
| Thu, 03 Nov 1994 16:52:19 +0100 |
lcp |
Pure/goals/prepare_proof/mkresult: now smashes flexflex pairs in the final
|
file |
diff |
annotate
|
| Wed, 02 Nov 1994 09:09:30 +0100 |
nipkow |
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
|
file |
diff |
annotate
|
| Thu, 25 Aug 1994 10:41:17 +0200 |
lcp |
print_sign_exn: now exported, with a polymorphic type
|
file |
diff |
annotate
|
| Thu, 18 Aug 1994 17:53:28 +0200 |
lcp |
Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
|
file |
diff |
annotate
|
| Thu, 03 Feb 1994 13:55:20 +0100 |
wenzelm |
replaced eq_sg by Sign.eq_sg;
|
file |
diff |
annotate
|
| Tue, 18 Jan 1994 15:57:40 +0100 |
lcp |
Many other files modified as follows:
|
file |
diff |
annotate
|
| Fri, 22 Oct 1993 10:31:19 +0100 |
lcp |
goals/print_top,prepare_proof: now call \!print_goals_ref
|
file |
diff |
annotate
|
| Fri, 08 Oct 1993 12:30:01 +0100 |
wenzelm |
"The error/exception above ...": errorneous goal now quoted;
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|