| Thu, 11 Jun 2015 00:13:25 +0100 | paulson | Merge | changeset | files |
| Thu, 11 Jun 2015 00:12:27 +0100 | paulson | tidied more proofs | changeset | files |
| Wed, 10 Jun 2015 23:34:23 +0200 | wenzelm | misc tuning; | changeset | files |
| Wed, 10 Jun 2015 22:28:56 +0200 | wenzelm | misc tuning; | changeset | files |
| Wed, 10 Jun 2015 21:49:02 +0200 | wenzelm | unused; | changeset | files |
| Wed, 10 Jun 2015 20:15:58 +0200 | wenzelm | misc tuning; | changeset | files |
| Wed, 10 Jun 2015 19:10:20 +0200 | wenzelm | isabelle update_cartouches; | changeset | files |
| Wed, 10 Jun 2015 19:05:19 +0200 | wenzelm | more user aliases; | changeset | files |
| Wed, 10 Jun 2015 18:57:31 +0200 | wenzelm | merged | changeset | files |
| Wed, 10 Jun 2015 18:48:48 +0200 | wenzelm | prefer direct Assumption.add_assms -- avoid term bindings of Proof_Context.add_assms; | changeset | files |
| Wed, 10 Jun 2015 17:22:35 +0200 | wenzelm | tuned proofs; | changeset | files |
| Wed, 10 Jun 2015 16:09:49 +0200 | wenzelm | clarified local after_qed: result is not exported yet; | changeset | files |
| Wed, 10 Jun 2015 14:46:31 +0200 | wenzelm | support for "if prems" in local goal statements; | changeset | files |
| Wed, 10 Jun 2015 11:52:54 +0200 | wenzelm | tuned message; | changeset | files |
| Wed, 10 Jun 2015 11:14:46 +0200 | wenzelm | tuned proofs; | changeset | files |
| Wed, 10 Jun 2015 11:14:04 +0200 | wenzelm | no need for protected goal (see 240ad53041c9); | changeset | files |
| Wed, 10 Jun 2015 10:39:28 +0200 | wenzelm | tuned proofs; | changeset | files |
| Wed, 10 Jun 2015 10:29:32 +0200 | wenzelm | prevent export of future result -- avoid interference with goal fixes; | changeset | files |
| Tue, 09 Jun 2015 22:24:33 +0200 | wenzelm | more uniform treatment of auto bindings vs. explicit user bindings; | changeset | files |
| Tue, 09 Jun 2015 16:42:17 +0200 | wenzelm | tuned signature; | changeset | files |
| Tue, 09 Jun 2015 16:07:11 +0200 | wenzelm | allow for_fixes for 'have', 'show' etc.; | changeset | files |
| Tue, 09 Jun 2015 15:28:06 +0200 | wenzelm | eliminated dead code; | changeset | files |
| Tue, 09 Jun 2015 13:42:58 +0200 | wenzelm | clarified abstracted term bindings (again, see c8384ff11711); | changeset | files |
| Tue, 09 Jun 2015 12:32:01 +0200 | wenzelm | tuned signature; | changeset | files |
| Tue, 09 Jun 2015 12:17:50 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 09 Jun 2015 11:51:05 +0200 | wenzelm | clarified term bindings; | changeset | files |
| Wed, 10 Jun 2015 15:50:17 +0200 | fleury | tuned | changeset | files |
| Wed, 10 Jun 2015 13:44:46 +0200 | Mathias Fleury | Merge | changeset | files |
| Wed, 10 Jun 2015 13:38:19 +0200 | Mathias Fleury | tuned | changeset | files |
| Wed, 10 Jun 2015 13:24:16 +0200 | Mathias Fleury | Renaming multiset operators < ~> <#,... | changeset | files |
| Tue, 09 Jun 2015 22:48:11 +0100 | paulson | more tidying up of proofs | changeset | files |
| Mon, 08 Jun 2015 23:52:21 +0100 | paulson | tidying messy proofs | changeset | files |
| Mon, 08 Jun 2015 23:51:08 +0100 | paulson | tidying messy proofs | changeset | files |
| Mon, 08 Jun 2015 22:04:19 +0200 | wenzelm | merged | changeset | files |
| Mon, 08 Jun 2015 22:04:15 +0200 | wenzelm | clarified context; | changeset | files |
| Mon, 08 Jun 2015 21:39:16 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 08 Jun 2015 21:23:28 +0200 | wenzelm | clarified abstracted term bindings; | changeset | files |
| Mon, 08 Jun 2015 20:58:43 +0200 | wenzelm | avoid duplicate warning due to Variable.warn_extra_tfrees; | changeset | files |
| Mon, 08 Jun 2015 20:53:42 +0200 | wenzelm | clarified Proof_Context.cert_propp/read_propp; | changeset | files |
| Mon, 08 Jun 2015 19:38:08 +0200 | wenzelm | more careful treatment of term bindings in 'obtain' proof body; | changeset | files |
| Mon, 08 Jun 2015 14:45:31 +0200 | wenzelm | tuned signature; | changeset | files |
| Mon, 08 Jun 2015 18:56:04 +0100 | paulson | Merge | changeset | files |
| Mon, 08 Jun 2015 00:25:10 +0100 | paulson | Tidied lots of messy proofs | changeset | files |
| Sun, 07 Jun 2015 23:37:32 +0200 | wenzelm | tuned signature; | changeset | files |
| Sun, 07 Jun 2015 22:04:50 +0200 | wenzelm | tuned (see also 66e6c539a36d); | changeset | files |
| Sun, 07 Jun 2015 21:58:18 +0200 | wenzelm | tuned signature; | changeset | files |
| Sun, 07 Jun 2015 21:30:53 +0200 | wenzelm | clarified: declare props once and for all; | changeset | files |
| Sun, 07 Jun 2015 20:03:40 +0200 | wenzelm | tuned signature; | changeset | files |
| Sun, 07 Jun 2015 15:35:49 +0200 | wenzelm | tuned signature; | changeset | files |
| Sun, 07 Jun 2015 15:01:07 +0200 | wenzelm | tuned signature; | changeset | files |
| Sun, 07 Jun 2015 14:36:36 +0200 | wenzelm | tuned; | changeset | files |
| Sun, 07 Jun 2015 12:55:42 +0200 | wenzelm | tuned; | changeset | files |
| Sun, 07 Jun 2015 12:55:28 +0200 | wenzelm | tuned; | changeset | files |
| Sun, 07 Jun 2015 12:43:06 +0200 | wenzelm | tuned whitespace; | changeset | files |
| Sat, 06 Jun 2015 13:38:24 +0200 | wenzelm | more tight treatment of subgoals: main goal may refer to extra variables; | changeset | files |
| Fri, 05 Jun 2015 13:41:06 +0200 | wenzelm | added Isar command 'supply'; | changeset | files |
| Fri, 05 Jun 2015 13:26:12 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 05 Jun 2015 11:11:26 +0200 | wenzelm | clarified signature -- better support for Isar commands outside of Pure; | changeset | files |
| Wed, 03 Jun 2015 21:48:40 +0200 | wenzelm | merged | changeset | files |
| Wed, 03 Jun 2015 19:25:05 +0200 | wenzelm | clarified context; | changeset | files |