| Wed, 28 Nov 2018 12:17:42 +0100 |
Walther Neuper |
cleanup leftover
|
changeset |
files
|
| Wed, 28 Nov 2018 11:46:00 +0100 |
Walther Neuper |
funpack: separate programs in prep. for partial_function
|
changeset |
files
|
| Wed, 21 Nov 2018 12:32:54 +0100 |
Walther Neuper |
update to new Isabelle conventions: {*...*} to \<open>...\<close>
|
changeset |
files
|
| Wed, 05 Sep 2018 18:09:56 +0200 |
Walther Neuper |
/----- finish update Isabelle2017->18: for Test_Isac.thy
|
changeset |
files
|
| Wed, 05 Sep 2018 15:34:39 +0200 |
Walther Neuper |
Isabelle2017->18: use libisabelle as separate session
|
changeset |
files
|
| Tue, 04 Sep 2018 14:50:30 +0200 |
Walther Neuper |
Isabelle2017->18: add libisabelle, PROBLEM with session management:
|
changeset |
files
|
| Wed, 29 Aug 2018 11:27:22 +0200 |
Walther Neuper |
------ finish update Isabelle2017 --> Isabelle2018 for Test_Isac.thy
|
changeset |
files
|
| Wed, 29 Aug 2018 11:24:41 +0200 |
Walther Neuper |
Isabelle2017->18: in term language "op" replaced by "lambda"
|
changeset |
files
|
| Tue, 28 Aug 2018 14:04:25 +0200 |
Walther Neuper |
Isabelle2017->18: intermediate repair cf. 7b2998e11662
|
changeset |
files
|
| Tue, 28 Aug 2018 13:34:22 +0200 |
Walther Neuper |
Isabelle2017->18: adapt to more rigorous session handling
|
changeset |
files
|
| Tue, 28 Aug 2018 11:34:55 +0200 |
Walther Neuper |
Isabelle2017->18: avoid libisabelle ERROR in ROOT, cf.7b2998e11662
|
changeset |
files
|
| Mon, 27 Aug 2018 17:14:23 +0200 |
Walther Neuper |
Isabelle2017->18: Test_Isac.thy for request at isabelle-users@
|
changeset |
files
|
| Mon, 27 Aug 2018 15:57:45 +0200 |
Walther Neuper |
sabelle2017->18: for Test_Isac.thy minor changes
|
changeset |
files
|
| Fri, 24 Aug 2018 14:23:13 +0200 |
Walther Neuper |
Isabelle2017->18: for Test_Isac.thy adopt new comments
|
changeset |
files
|
| Fri, 24 Aug 2018 13:05:00 +0200 |
Walther Neuper |
Isabelle2017->18: for Test_Isac.thy adapt new form of imports
|
changeset |
files
|
| Thu, 23 Aug 2018 17:23:11 +0200 |
Walther Neuper |
/----- finish update Isabelle2017 --> Isabelle2018
|
changeset |
files
|
| Thu, 23 Aug 2018 17:20:37 +0200 |
Walther Neuper |
Isabelle2017->18: bypass libisabelle (search libisabelle_DUMMY), Build_Isac.thy OK
|
changeset |
files
|
| Thu, 23 Aug 2018 11:01:03 +0200 |
Walther Neuper |
Isabelle2017->18: ProgLang, Interpret compile
|
changeset |
files
|
| Thu, 23 Aug 2018 09:42:19 +0200 |
Walther Neuper |
Isabelle2017->18: Pure and HOL build with updated thm.ML
|
changeset |
files
|
| Thu, 23 Aug 2018 09:38:26 +0200 |
Walther Neuper |
Isabelle20XX->YY: insert Isac's hooks in ~~/src/Pure/thm.ML
|
changeset |
files
|
| Thu, 23 Aug 2018 09:28:04 +0200 |
Walther Neuper |
Isabelle2017->18: separate appearance of Isac from Isabelle
|
changeset |
files
|
| Wed, 22 Aug 2018 15:44:30 +0200 |
Walther Neuper |
Isabelle20XX->YY: notify Isabelle about Isac
|
changeset |
files
|
| Wed, 22 Aug 2018 15:42:55 +0200 |
Walther Neuper |
Isabelle2017->18: specify root for ~/.isabelle/
|
changeset |
files
|
| Wed, 22 Aug 2018 14:44:15 +0200 |
Walther Neuper |
\----- start update Isabelle2017 --> Isabelle2018
|
changeset |
files
|
| Wed, 22 Aug 2018 12:47:53 +0200 |
Walther Neuper |
Added tag isabisac17 for changeset 5535bdba43b6
|
changeset |
files
|
| Wed, 22 Aug 2018 12:47:25 +0200 |
Walther Neuper |
final isabisac17 on Isabelle2017
isabisac17
|
changeset |
files
|
| Wed, 22 Aug 2018 10:19:32 +0200 |
Walther Neuper |
isac-jEdit: withdraw inappropriate trial to learn from ML_Lex.read_source
|
changeset |
files
|
| Wed, 22 Aug 2018 09:47:46 +0200 |
Walther Neuper |
isac-jEdit: intermediately stopped
|
changeset |
files
|
| Tue, 03 Jul 2018 12:32:24 +0200 |
Walther Neuper |
isac-jEdit: prepare for parsing Isac problems
|
changeset |
files
|
| Tue, 03 Jul 2018 08:54:35 +0200 |
Walther Neuper |
bridge: create "minor keywords" which can occur within scope of a "majore keyword"
|
changeset |
files
|
| Tue, 03 Jul 2018 08:51:57 +0200 |
Walther Neuper |
bridge: make example for parsing accessible
|
changeset |
files
|
| Sat, 16 Jun 2018 07:45:52 +0200 |
Walther Neuper |
bridge: start calculation (command def. without semantics)
|
changeset |
files
|
| Sat, 16 Jun 2018 07:42:24 +0200 |
Walther Neuper |
bridge: replace strings by cartouches in example
|
changeset |
files
|
| Wed, 13 Jun 2018 08:14:26 +0200 |
Walther Neuper |
bridge: more suitable command types, probably
|
changeset |
files
|
| Tue, 12 Jun 2018 14:53:47 +0200 |
Walther Neuper |
partial_function: found examples
|
changeset |
files
|
| Tue, 12 Jun 2018 10:25:27 +0200 |
Walther Neuper |
bridge: complete list of commands
|
changeset |
files
|
| Tue, 12 Jun 2018 08:08:16 +0200 |
Walther Neuper |
bridge: comment on templates
|
changeset |
files
|
| Mon, 11 Jun 2018 16:28:21 +0200 |
Walther Neuper |
bridge: hint by Makarius how to introduce templates
|
changeset |
files
|
| Mon, 11 Jun 2018 16:07:53 +0200 |
Walther Neuper |
bridge: start with SPARK as a model
|
changeset |
files
|
| Sat, 26 May 2018 14:58:37 +0200 |
Walther Neuper |
bridge: copy ML scanner to isac scanner
|
changeset |
files
|
| Sat, 26 May 2018 14:16:37 +0200 |
Walther Neuper |
bridge: Makarius' hints by mail
|
changeset |
files
|
| Sat, 26 May 2018 11:26:43 +0200 |
Walther Neuper |
bridge: introduce Isabelle/jEdit as Isac front-end, begin
|
changeset |
files
|
| Sat, 26 May 2018 11:13:36 +0200 |
Walther Neuper |
cleanup Test.thy partially
|
changeset |
files
|
| Fri, 18 May 2018 18:32:02 +0200 |
Walther Neuper |
rm global ref from Test.thy finally
|
changeset |
files
|
| Fri, 18 May 2018 17:59:48 +0200 |
Walther Neuper |
partial_function: clean Test.thy partially
|
changeset |
files
|
| Wed, 11 Apr 2018 14:44:46 +0200 |
Walther Neuper |
partial_function: start cleaning programs, biegelinie for paper
|
changeset |
files
|
| Wed, 04 Apr 2018 12:41:03 +0200 |
Walther Neuper |
clean theory dependencies, finished: Test_Isac ok
|
changeset |
files
|
| Tue, 03 Apr 2018 17:29:54 +0200 |
Walther Neuper |
clean theory dependencies, partially
|
changeset |
files
|
| Tue, 03 Apr 2018 16:53:18 +0200 |
Walther Neuper |
improve test suite
|
changeset |
files
|
| Tue, 03 Apr 2018 15:48:39 +0200 |
Walther Neuper |
partial_function: Test_Isac OK again
|
changeset |
files
|
| Tue, 03 Apr 2018 14:50:58 +0200 |
Walther Neuper |
partial_function: shift respective thys to ProgLang
|
changeset |
files
|
| Sat, 31 Mar 2018 10:30:17 +0200 |
Walther Neuper |
create browser_info
|
changeset |
files
|
| Mon, 26 Mar 2018 16:27:43 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Mon, 26 Mar 2018 16:25:01 +0200 |
Walther Neuper |
LibraryC: clean source file done
|
changeset |
files
|
| Mon, 26 Mar 2018 14:20:57 +0200 |
Walther Neuper |
LibraryC: clean source file, partially
|
changeset |
files
|
| Mon, 26 Mar 2018 10:21:19 +0200 |
Walther Neuper |
introduce structure LibraryC
|
changeset |
files
|
| Mon, 26 Mar 2018 09:27:24 +0200 |
Walther Neuper |
Rule + Celem: notes on futher cleanup
|
changeset |
files
|
| Mon, 26 Mar 2018 09:20:09 +0200 |
Walther Neuper |
Rule: Test_Isac works completely
|
changeset |
files
|
| Mon, 26 Mar 2018 07:28:39 +0200 |
Walther Neuper |
Rule: structure pushed to code files
|
changeset |
files
|
| Sun, 25 Mar 2018 13:59:57 +0200 |
Walther Neuper |
Celem: separate structure Rule
|
changeset |
files
|