| Sun, 18 Apr 2021 13:10:25 +0200 |
wenzelm |
obsolete: no need to patch official thm.ML;
|
changeset |
files
|
| Sun, 18 Apr 2021 13:11:05 +0200 |
Walther Neuper |
merged
|
changeset |
files
|
| Sun, 18 Apr 2021 12:42:27 +0200 |
Walther Neuper |
merged
|
changeset |
files
|
| Sun, 18 Apr 2021 12:42:22 +0200 |
Walther Neuper |
user requirements on terms continued
|
changeset |
files
|
| Sun, 18 Apr 2021 13:01:05 +0200 |
wenzelm |
implement sym_thm as proper infernce rule:
|
changeset |
files
|
| Sat, 17 Apr 2021 21:37:31 +0200 |
wenzelm |
more conservative numerals_to_Free: prefer existing Skip_Proof.make_thm (which assumes that thms are in standard form);
|
changeset |
files
|
| Sat, 17 Apr 2021 21:20:56 +0200 |
wenzelm |
prefer existing Skip_Proof.make_thm;
|
changeset |
files
|
| Sat, 17 Apr 2021 21:10:27 +0200 |
wenzelm |
more direct use of Thm.prop_of;
|
changeset |
files
|
| Sat, 17 Apr 2021 20:44:57 +0200 |
wenzelm |
remove generated file from repository;
|
changeset |
files
|
| Sat, 17 Apr 2021 20:42:45 +0200 |
wenzelm |
merged;
|
changeset |
files
|
| Sat, 17 Apr 2021 20:41:09 +0200 |
wenzelm |
avoid changes to Isabelle sources:
|
changeset |
files
|
| Sat, 17 Apr 2021 20:37:13 +0200 |
wenzelm |
avoid experimental changes to Isabelle sources;
|
changeset |
files
|
| Sat, 17 Apr 2021 18:44:27 +0200 |
Walther Neuper |
deleted ~~/contrib
|
changeset |
files
|
| Sat, 17 Apr 2021 18:35:43 +0200 |
Walther Neuper |
user requirements on terms
|
changeset |
files
|
| Sat, 17 Apr 2021 17:53:30 +0200 |
wenzelm |
make this appear like a repository clone of Isabelle2021 --- with proper Admin directory (e.g. required to build jars on the spot);
|
changeset |
files
|
| Sat, 17 Apr 2021 17:51:44 +0200 |
wenzelm |
proper file name;
|
changeset |
files
|
| Sat, 17 Apr 2021 17:49:46 +0200 |
wenzelm |
add missing files;
|
changeset |
files
|
| Fri, 16 Apr 2021 23:57:40 +0200 |
wenzelm |
missing file from Isabelle2021;
|
changeset |
files
|
| Fri, 16 Apr 2021 22:29:23 +0200 |
wenzelm |
prefer symbolic directories $ISABELLE_ISAC and $ISABELLE_ISAC_TEST, instead of re-using ~~ for $ISABELLE_HOME;
|
changeset |
files
|
| Fri, 16 Apr 2021 22:13:43 +0200 |
wenzelm |
more explicit components;
|
changeset |
files
|
| Tue, 13 Apr 2021 14:07:17 +0200 |
Walther Neuper |
repair setup for session "Doc" cf.751b8a13c271
|
changeset |
files
|
| Tue, 13 Apr 2021 13:20:05 +0200 |
Walther Neuper |
trial with setup for session "Doc", unsuccessful
|
changeset |
files
|
| Thu, 08 Apr 2021 13:27:27 +0200 |
wenzelm |
avoid odd clones of Isabelle latex styles:
|
changeset |
files
|
| Thu, 08 Apr 2021 13:09:44 +0200 |
wenzelm |
proper setup for "Doc" sessions;
|
changeset |
files
|
| Mon, 22 Mar 2021 14:47:06 +0100 |
wenzelm |
do not suppress etc/settings: important for Isabelle component setup;
|
changeset |
files
|
| Wed, 07 Apr 2021 21:33:01 +0200 |
Walther Neuper |
pwd test by WN
|
changeset |
files
|
| Tue, 06 Apr 2021 15:52:27 +0200 |
Walther Neuper |
add text for Specify_Phase
|
changeset |
files
|
| Sun, 04 Apr 2021 13:31:04 +0200 |
Walther Neuper |
new session for Doc/Specify_Phase, incomplete
|
changeset |
files
|
| Sun, 04 Apr 2021 12:29:42 +0200 |
Walther Neuper |
separate session Specify
|
changeset |
files
|
| Sat, 03 Apr 2021 15:27:52 +0200 |
Walther Neuper |
review and update directories in Build_Isac
|
changeset |
files
|
| Mon, 22 Mar 2021 17:22:08 +0100 |
Walther Neuper |
tuned
|
changeset |
files
|
| Mon, 22 Mar 2021 16:20:56 +0100 |
Walther Neuper |
remove notes from Calculation.thy
|
changeset |
files
|
| Mon, 22 Mar 2021 08:31:30 +0100 |
Walther Neuper |
remove outdated comments and trials
|
changeset |
files
|
| Thu, 18 Mar 2021 13:56:45 +0100 |
Walther Neuper |
Example takes a single file
|
changeset |
files
|
| Mon, 15 Mar 2021 10:49:53 +0100 |
Walther Neuper |
resume step 6.10: unsuccessful trials with combination of types on Outer_Syntax
|
changeset |
files
|
| Mon, 15 Mar 2021 10:45:12 +0100 |
Walther Neuper |
/----- finish update Isabelle2020 --> Isabelle2021 for Test_Isac_Short.thy
|
changeset |
files
|
| Mon, 15 Mar 2021 10:04:17 +0100 |
Walther Neuper |
Isabelle2020->21: th_load with constant string
|
changeset |
files
|
| Fri, 12 Mar 2021 15:22:39 +0100 |
Walther Neuper |
Isabelle2020->21: declare "thy_load (isac_example)" to Scala, partially
|
changeset |
files
|
| Fri, 12 Mar 2021 13:25:51 +0100 |
Walther Neuper |
Isabelle2020->21: adapt SPARK to tests
|
changeset |
files
|
| Fri, 12 Mar 2021 12:48:55 +0100 |
Walther Neuper |
Isabelle2020->21: adapt SPARK to ParseC
|
changeset |
files
|
| Mon, 08 Mar 2021 10:04:37 +0100 |
Walther Neuper |
Isabelle2020->21: Pure and HOL build with updated thm.ML
|
changeset |
files
|
| Mon, 08 Mar 2021 09:43:59 +0100 |
Walther Neuper |
Isabelle2020->21: separate appearance of Isac from Isabelle
|
changeset |
files
|
| Mon, 08 Mar 2021 09:40:09 +0100 |
Walther Neuper |
Isabelle2020->21: notify Isabelle about Isac sessions
|
changeset |
files
|
| Mon, 08 Mar 2021 09:35:14 +0100 |
Walther Neuper |
Isabelle2020->21: define storage for installation-specific settings
|
changeset |
files
|
| Mon, 08 Mar 2021 09:11:09 +0100 |
Walther Neuper |
\----- start update Isabelle2020 --> Isabelle2021
|
changeset |
files
|
| Mon, 08 Mar 2021 08:42:05 +0100 |
Walther Neuper |
Added tag isabisac20 for changeset 573da5c3a9f6
|
changeset |
files
|
| Mon, 08 Mar 2021 08:41:45 +0100 |
Walther Neuper |
final isabisac20 on Isabelle2020
isabisac20
|
changeset |
files
|
| Mon, 08 Mar 2021 08:17:28 +0100 |
Walther Neuper |
step 6.10: stop unsuccessful trials with combination of types on Outer_Syntax
|
changeset |
files
|
| Mon, 01 Mar 2021 16:03:06 +0100 |
Walther Neuper |
step 6.9: errors on Given, RTheory due to "Model" "References" :: diag
|
changeset |
files
|
| Mon, 01 Mar 2021 12:46:40 +0100 |
Walther Neuper |
step 6.8: "Specification" "Model" :: diag ..both work,
|
changeset |
files
|
| Sat, 27 Feb 2021 16:59:41 +0100 |
Walther Neuper |
step 6.7: new error on Specification:
|
changeset |
files
|
| Sat, 27 Feb 2021 16:35:33 +0100 |
Walther Neuper |
step 6.7: describe error on Specification:
|
changeset |
files
|
| Fri, 26 Feb 2021 19:20:50 +0100 |
Walther Neuper |
step 6.6: prelim. Outer_Syntax..Specification, Model, Given, ..
|
changeset |
files
|
| Fri, 26 Feb 2021 13:13:03 +0100 |
Walther Neuper |
step 6.5: investigate collision Problem .. Specification; Position?
|
changeset |
files
|
| Wed, 17 Feb 2021 15:43:34 +0100 |
Walther Neuper |
step 6.4 ~ step 3.5: make Problem independent from SPARK
|
changeset |
files
|
| Thu, 11 Feb 2021 17:45:29 +0100 |
Walther Neuper |
step 6.3: prep. clean Outer_Syntax..Problem from SPARK code
|
changeset |
files
|
| Wed, 03 Feb 2021 16:39:44 +0100 |
Walther Neuper |
Isac's MethodC not shadowing Isabelle's Method
|
changeset |
files
|
| Wed, 03 Feb 2021 15:21:12 +0100 |
Walther Neuper |
step 6.2: check test-Example: same errors with ParseC.problem .. ParseC.problem_headline
|
changeset |
files
|
| Wed, 03 Feb 2021 14:53:37 +0100 |
Walther Neuper |
step 5.1: adapt ParseC.specification to new keywords
|
changeset |
files
|
| Tue, 26 Jan 2021 12:46:12 +0100 |
Walther Neuper |
step 6> use SPARK as a model for checking input to Model
|
changeset |
files
|