| Wed, 30 Oct 2019 16:46:05 +0100 |
lucin: remove remaining Pstate exhibiting internal structure
|
file | diff | annotate |
| Fri, 25 Oct 2019 16:07:15 +0200 |
lucin: adopt Poly/ML warnings in lucas-interpreter.sml
|
file | diff | annotate |
| Sat, 19 Oct 2019 18:19:16 +0200 |
lucin: introduce interpreter-state to appy & Co
|
file | diff | annotate |
| Sat, 19 Oct 2019 14:07:27 +0200 |
tuned
|
file | diff | annotate |
| Thu, 17 Oct 2019 13:17:48 +0200 |
lucin: cleanup args in lucas-interpreter, preps
|
file | diff | annotate |
| Wed, 28 Aug 2019 11:21:26 +0200 |
reorganised MathEngine/ BridgeLibisabelle/
|
file | diff | annotate |
| Tue, 27 Aug 2019 18:03:33 +0200 |
assign Input_Descript to Specify/-phase
|
file | diff | annotate |
| Tue, 27 Aug 2019 11:59:48 +0200 |
separate Specify/ from Interpret/
|
file | diff | annotate |
| Wed, 24 Jul 2019 11:30:59 +0200 |
lucin: separate interpreter-state and improve type-identifier
|
file | diff | annotate |
| Wed, 24 Jul 2019 09:32:17 +0200 |
lucin: improve signature of "fun locate_input_tactic"
|
file | diff | annotate |
| Mon, 24 Jun 2019 14:02:39 +0200 |
[-Test_Isac] lucin: shift "find next tactic" into lucas-interpreter.sml
|
file | diff | annotate |
| Wed, 21 Nov 2018 12:32:54 +0100 |
update to new Isabelle conventions: {*...*} to \<open>...\<close>
|
file | diff | annotate |
| Tue, 07 Feb 2017 08:57:42 +0100 |
separate structure Model : MODEL
|
file | diff | annotate |
| Mon, 06 Feb 2017 09:06:35 +0100 |
improved CLEANUP
|
file | diff | annotate |
| Mon, 06 Feb 2017 09:00:32 +0100 |
tuned
|
file | diff | annotate |
| Sat, 04 Feb 2017 07:20:39 +0100 |
separate structure Stool : SPECIFY_TOOL
|
file | diff | annotate |
| Sat, 21 Jan 2017 10:25:19 +0100 |
prep 1 for structure Tac : TACTIC
|
file | diff | annotate |
| Wed, 18 Jan 2017 09:09:04 +0100 |
begin to divide structure Ctree
|
file | diff | annotate |
| Fri, 06 Jan 2017 14:48:20 +0100 |
further preparation for separating ctree-basic.sml
|
file | diff | annotate |
| Wed, 28 Dec 2016 13:07:17 +0100 |
replaced ctree.sml by basic-ctree.sml before separation
|
file | diff | annotate |
| Wed, 28 Dec 2016 08:57:00 +0100 |
clean structure Applicable
|
file | diff | annotate |
| Tue, 27 Dec 2016 17:43:12 +0100 |
demo ERROR: declare [[ML_print_depth = 999]] kills Isabelle/Isac
|
file | diff | annotate |
| Tue, 27 Dec 2016 13:20:33 +0100 |
clean structure Ctree continued
|
file | diff | annotate |
| Thu, 22 Dec 2016 11:36:20 +0100 |
renamed Ctree.ptree --> Ctree.ctree
|
file | diff | annotate |
| Wed, 30 Nov 2016 12:09:24 +0100 |
added structure Rtools : REWRITE_TOOLS
|
file | diff | annotate |
| Thu, 20 Oct 2016 10:26:29 +0200 |
simplify handling of theorems
|
file | diff | annotate |
| Tue, 18 Oct 2016 12:05:03 +0200 |
back-track after desing error in previous changeset
|
file | diff | annotate |
| Mon, 10 Oct 2016 18:24:14 +0200 |
transport terms in theorems to frontend
|
file | diff | annotate |
| Thu, 21 Nov 2013 11:17:42 +0100 |
Isabelle2013 --> 2013-1: remove left-over legacy "uses" "axiom"
|
file | diff | annotate |
| Sun, 16 Jun 2013 12:31:41 +0200 |
Isabelle2011 --> 2012 intermediate
|
file | diff | annotate |
| Fri, 12 Oct 2012 17:06:58 +0200 |
2011-->2012: ProofContext-->Proof_Context
|
file | diff | annotate |
| Wed, 23 Mar 2011 17:20:39 +0100 |
make Test_Isac.thy run in jEdit; intermed.
|
file | diff | annotate |
| Tue, 01 Mar 2011 15:23:59 +0100 |
intermed.update to Isabelle2011: test/../syntax added
|
file | diff | annotate |