diff options
| author | Josh Chen | 2018-08-18 15:02:43 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-18 15:02:43 +0200 |
| commit | 8b767a5aac248892fb1a5ed99aca6699f5f2b317 (patch) | |
| tree | 883c1d9cfc901613bd033388544a18ea73f73ee6 | |
| parent | b0c85e7a4590e37d2b59d80106b993c3746445f0 (diff) | |
Rename
| -rw-r--r-- | tests/Subgoal.thy (renamed from tests/Schematic_subgoal.thy) | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tests/Schematic_subgoal.thy b/tests/Subgoal.thy index 5f20eac..2226f08 100644 --- a/tests/Schematic_subgoal.thy +++ b/tests/Subgoal.thy @@ -1,9 +1,10 @@ -theory Schematic_subgoal +theory Subgoal imports "../HoTT" begin text " \<open>subgoal\<close> converts schematic variables to fixed free variables, making it unsuitable for use in \<open>schematic_goal\<close> proofs. + This is the same thing as being unable to start a "sub-schematic goal" inside an ongoing proof. This is a problem for syntheses which need to use induction (elimination rules), as these often have to be applied to fixed variables, while keeping any schematic variables intact. " |